From f863978712caf71696279a37c9a600c94a92d80d Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Tue, 11 Aug 2009 16:03:46 +0000 Subject: [PATCH] made some changes to the MiniSAT Makefiles git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@104 e59a4935-1847-0410-ae03-e826735625c1 --- AST/AST.h | 3 +- AST/ToSAT.cpp | 15 +- Makefile.in | 7 +- bin/run_bigarray_tests | 537 +++++++++++++++++++++++++++++++++++++++++ sat/core/Main.C | 344 -------------------------- sat/core/Makefile | 3 + sat/mtl/template.mk | 2 +- sat/simp/Main.C | 415 ------------------------------- sat/simp/Makefile | 2 + sat/simp/SimpSolver.h | 90 +++---- sat/simp/depend.mk | 28 ++- 11 files changed, 616 insertions(+), 830 deletions(-) create mode 100755 bin/run_bigarray_tests delete mode 100644 sat/core/Main.C delete mode 100644 sat/simp/Main.C diff --git a/AST/AST.h b/AST/AST.h index a170dc5..2249651 100644 --- a/AST/AST.h +++ b/AST/AST.h @@ -32,7 +32,8 @@ #include #include "ASTUtil.h" #include "ASTKind.h" -#include "../sat/core/Solver.h" +//#include "../sat/core/Solver.h" +#include "../sat/simp/SimpSolver.h" #include "../sat/core/SolverTypes.h" #include #ifndef NATIVE_C_ARITH diff --git a/AST/ToSAT.cpp b/AST/ToSAT.cpp index 7a4aa1b..c99807a 100644 --- a/AST/ToSAT.cpp +++ b/AST/ToSAT.cpp @@ -138,15 +138,12 @@ void BeevMgr::PrintStats(MINISAT::Solver& s) return; double cpu_time = MINISAT::cpuTime(); uint64_t mem_used = MINISAT::memUsed(); - /* - reportf("restarts : %"I64_fmt"\n", s.starts); - reportf("conflicts : %-12"I64_fmt" (%.0f /sec)\n", s.conflicts , s.conflicts /cpu_time); - reportf("decisions : %-12"I64_fmt" (%.0f /sec)\n", s.decisions , s.decisions /cpu_time); - reportf("propagations : %-12"I64_fmt" (%.0f /sec)\n", s.propagations, s.propagations/cpu_time); - reportf("conflict literals : %-12"I64_fmt" (%4.2f %% deleted)\n", - s.tot_literals, - (s.max_literals - s.tot_literals)*100 / (double)s.max_literals); - */ + reportf("restarts : %llu\n", s.starts); + reportf("conflicts : %llu (%.0f /sec)\n", s.conflicts , s.conflicts /cpu_time); + reportf("decisions : %llu (%.0f /sec)\n", s.decisions , s.decisions /cpu_time); + reportf("propagations : %llu (%.0f /sec)\n", s.propagations, s.propagations/cpu_time); + reportf("conflict literals : %llu (%4.2f %% deleted)\n", s.tot_literals, + (s.max_literals - s.tot_literals)*100 / (double)s.max_literals); if (mem_used != 0) reportf("Memory used : %.2f MB\n", mem_used / 1048576.0); reportf("CPU time : %g s\n", cpu_time); diff --git a/Makefile.in b/Makefile.in index faec41c..1b99b56 100644 --- a/Makefile.in +++ b/Makefile.in @@ -19,13 +19,14 @@ HEADERS=c_interface/*.h .PHONY: all all: $(MAKE) -C AST - $(MAKE) -C sat/core lib + $(MAKE) -C sat core $(MAKE) -C simplifier $(MAKE) -C bitvec $(MAKE) -C c_interface $(MAKE) -C constantbv $(MAKE) -C parser - $(AR) rc libstp.a AST/*.o sat/core/*.or simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o parser/let-funcs.o parser/parseCVC.o parser/lexCVC.o + #$(AR) rc libstp.a AST/*.o sat/core/*.or simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o parser/let-funcs.o parser/parseCVC.o parser/lexCVC.o + $(AR) rc libstp.a AST/*.o sat/*.a simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o parser/let-funcs.o parser/parseCVC.o parser/lexCVC.o $(RANLIB) libstp.a @mkdir -p lib @mv libstp.a lib/ @@ -55,7 +56,7 @@ clean: #rm -rf config.info rm -f TAGS $(MAKE) clean -C AST - $(MAKE) clean -C sat/core + $(MAKE) clean -C sat $(MAKE) clean -C simplifier $(MAKE) clean -C bitvec $(MAKE) clean -C parser diff --git a/bin/run_bigarray_tests b/bin/run_bigarray_tests new file mode 100755 index 0000000..4656ac8 --- /dev/null +++ b/bin/run_bigarray_tests @@ -0,0 +1,537 @@ +#!/usr/bin/perl -w + +# Run STP regression tests of a given level (default: 0, meaning +# minimum amount of tests). The higher the regression level, the more +# tests to run, and the harder they get. +# Each test may contain information about its regression level, +# expected outcome, expected runtime, whether it produces a proof, +# etc. in the format given below. This script will scan the first 100 +# lines of each test and try to collect this information. + +# If some info is not found, defaults are assumed. Default regression +# level is 0, expected runtime is unbounded, outcome is undefined +# (whatever it returns is OK), proof should be produced if outcome is +# Valid, and if it is produced, it'll be verified. + +# Test info is given in the comments; here are examples +# +# %%% Regression level = 2 +# %%% Result = Valid %% or Invalid, or Unknown +# %%% Runtime = 10 %% in seconds +# %%% Proof = yes %% or 'no', if it doesn't produce a proof +# %%% Language = presentation %% or 'internal' + +# The number of '%' and following spaces can vary, case is not +# important. Any text after the value is ignored. Any comments that +# are not recognized are also ignored. + +use strict; + +my %optionsHelp = + ("-h" => "Print this help and exit", + "-v" => "Be verbose (default, opposite of -q)", + "-q" => "Quiet mode (opposite of -v)", + "-l n" => "Set regression level (default 0, the easiest level)", + "+rt" => "Check that each test finishes within the specified runtime", + "-rt" => "Do not check whether test finishes within the specified runtime (default)", +# "+proofs" => "Produce and verify proofs", +# "-proofs" => "Do not produce / verify proofs (default)", + "-lang name" => "Use the named input language only (default=all)", + "-t secs" => "Run each executable for at most 'secs' seconds [0 = no limit]", + "-vc prog" => "Use \"prog\" to run STP (default=bin/stp)", + "-pfc prog" => "Use \"prog\" to run a proof checker (default=true)" + ); + +my $usageString = + "run_tests [ options ] [ test1 test2 ... ] [ -- [ stp options ] ] + +Run STP Lite regression tests. Concrete test files or directories +with test files should be specified by name with a full path or +relative path to the current directory. If none specified, all +subdirectories are searched for test files. + +Default running mode is overriden by test specs; +test specs are overriden by command line options. + +Options: + " . join("\n ", + map { sprintf("%-9s %s", $_, $optionsHelp{$_}) } keys(%optionsHelp)); + +my $pwd = `pwd` ; +chomp $pwd ; + +# Database of default values for options +my %optionsDefault = ("level" => 4, + "verbose" => 1, + "rt" => 1, + "proofs" => 0, + "lang" => "all", + "stppath" => "stp/bin", + "vc" => $pwd . "/bin/stp -d", # Program names + #"vc" => "valgrind --leak-check=full /home/vganesh/stp/bin/stp", # Program names + "pfc" => "true", + "stptestpath" => "stp/test", + "stptemp" => "/tmp", + # max. number of lines to read from the testcase file + # when looking for info comments + "maxInfoLines" => 4, + # Runtime limit; 0 = no limit + "time" => 180, + # Additional command line options to stp + "stpOptions" => "-d"); + +# Database of command line options. Initially, they are undefined +my %options = (); +# The list of testcases to run +# +#my @testcases = "sample-tests"; +my @testcases = "../../stp-tests/bigarray-test"; +# Temporary array for STP options +my @stpOptions = (); +# State is either "own" or "stp", meaning that we're reading either +# our own or stp's options. +my $argState = "own"; +# for(my $i=0; $i <= $#ARGV; $i++) { +# if($argState eq "own") { +# if($ARGV[$i] eq "--") { $argState = "stp"; } +# elsif($ARGV[$i] eq "-h") { print($usageString, "\n"); exit 0; } +# elsif($ARGV[$i] eq "+rt") { $options{'rt'} = 1; } +# elsif($ARGV[$i] eq "-rt") { $options{'rt'} = 0; } +# elsif($ARGV[$i] eq "+proofs") { $options{'proofs'} = 1; } +# elsif($ARGV[$i] eq "-proofs") { $options{'proofs'} = 0; } +# elsif($ARGV[$i] eq "-v") { $options{'verbose'} = 1; } +# elsif($ARGV[$i] eq "-q") { $options{'verbose'} = 0; } +# elsif($ARGV[$i] eq "-lang") { +# if(++$i>$#ARGV) { +# print STDERR "Option -lang requires an argument.\n"; +# print STDERR "Run run_tests -h for help\n"; +# exit 1; +# } +# $options{'lang'} = $ARGV[$i]; +# } elsif($ARGV[$i] eq "-l") { +# if(++$i>$#ARGV) { +# print STDERR "Option -l requires an argument.\n"; +# print STDERR "Run run_tests -h for help\n"; +# exit 1; +# } +# $options{'level'} = $ARGV[$i]; +# } elsif($ARGV[$i] eq "-t") { +# if(++$i>$#ARGV) { +# print STDERR "Option -t requires an argument.\n"; +# print STDERR "Run run_tests -h for help\n"; +# exit 1; +# } +# $options{'time'} = $ARGV[$i]; +# } elsif($ARGV[$i] eq "-vc") { +# if(++$i>$#ARGV) { +# print STDERR "Option -vc requires an argument.\n"; +# print STDERR "Run run_tests -h for help\n"; +# exit 1; +# } +# $options{'vc'} = $ARGV[$i]; +# } elsif($ARGV[$i] eq "-pfc") { +# if(++$i>$#ARGV) { +# print STDERR "Option -pfc requires an argument.\n"; +# print STDERR "Run run_tests -h for help\n"; +# exit 1; +# } +# $options{'pfc'} = $ARGV[$i]; +# } else { +# # This must be a testcase name +# push @testcases, $ARGV[$i]; +# } +# } elsif($argState eq "stp") { +# push @stpOptions, $ARGV[$i]; +# } else { +# die "BUG: Bad argState: $argState"; +# } +# } + +if($#stpOptions >= 0) { + $options{'stpOptions'} = join(" ", map { "\"" . $_ . "\"" } @stpOptions); +} + +# Compute the value of the option: first check the command line +# option, then the supplied database (by ref. as the second arg), then +# default values database. If it cannot find definition, it is a bug, +# and the script is stopped. + +sub getOpt { + my ($name, $dbRef) = @_; + + return $options{$name} if(defined($options{$name})); + return $dbRef->{$name} if(defined($dbRef) && defined($dbRef->{$name})); + return $optionsDefault{$name} if(defined($optionsDefault{$name})); + + # Option value is not found + die "getOpt($name): option is undefined"; +} + +my $verbose = getOpt('verbose'); + +# Set the path +my $systemPath = "."; +if(defined($ENV{'PATH'})) { + $systemPath = $ENV{'PATH'}; +} +$ENV{'PATH'} = getOpt('stppath') . ":" . $systemPath; + +if($verbose) { + print "*********\n"; + print("Regression level: ", getOpt('level'), "\n"); + print("Language: ", getOpt('lang'), "\n"); + print("Whether to produce / check proofs: ", + (defined($options{'proofs'}))? + (($options{'proofs'})? "yes" : "no") : "depends on testcase", + "\n"); + if(getOpt('time') > 0) { + print("Time limit per test: ", getOpt('time'), " sec\n"); + } + print("PATH = ", $ENV{'PATH'}, "\n"); + print "*********\n"; +} + +my $tmpdir = getOpt('stptemp') . "/stptmp-$$"; +my $currdir = `pwd`; +my $stp = getOpt('vc'); +my $pfc = getOpt('pfc'); +my $level = getOpt('level'); +my $lang = getOpt('lang'); +my $rt = getOpt('rt'); + +# Read the first 'maxInfoLines' of the testcase and fetch information +# from the comments + +sub getTestOpt { + my ($name) = @_; + # This is what we return + my %db = (); + + open IN, $name or die "Cannot open $name: $?"; + for(my $lines = getOpt('maxInfoLines'), my $str = ; + defined($str) && $lines > 0; + $lines--, $str = ) + { + if($str =~ /^(\s|%|\#)*Regression level\s*=\s*(\d+)/i) { + $db{'level'} = $2; + } + if($str =~ /^(\s|%|\#)*Result\s*=\s*(Valid|Invalid|Unknown)/i) { + $db{'result'} = lc $2; + } + if($str =~ /^(\s|%|\#)*Runtime\s*=\s*(\d+)/i) { + $db{'runtime'} = $2; + } + if($str =~ /^(\s|%|\#)*Proof\s*=\s*(yes|no)/i) { + if($2 eq "yes") { $db{'proofs'} = 1; } + else { $db{'proofs'} = 0; } + } + if($str =~ /^(\s|%|\#)*SAT mode\s*=\s*(on|off)/i) { + if($2 eq "on") { $db{'sat'} = 1; } + else { $db{'sat'} = 0; } + } + if($str =~ /^(\s|%|\#)*Language\s*=\s*((\w|\d|\_)+)/i) { + $db{'lang'} = lc $2; + } + if($str =~ /^(\s|%|\#)*STP Options\s*=\s*(.*)$/i) { + $db{'stpOptions'} = $2; + } + } + close IN; + + # If regression level is not set, make it 3. So, if a lower level + # is requested, only explicitly marked tests will be run. + if(!defined($db{'level'})) { $db{'level'}=3; } + # If the input language is not defined, guess it by extension + if(!defined($db{'lang'})) { + if($name =~ /\.(stp|svc)$/) { + $db{'lang'} = "presentation"; + } elsif($name =~ /\.(li?sp)$/) { + $db{'lang'} = "internal"; + } elsif($name =~ /\.(smt)$/) { + $db{'lang'} = "smt-lib"; + } + } + + return %db; +} + +# Total number of tests run +my $testsTotal=0; +# Total number of proofs checked by pfc +my $proofsChecked=0; +# Total number of tests with problems (each test is counted at most once) +my $testsProblems=0; +### Database of results +# It is a hash mapping problem keys to arrays of testcase names. +# Only problematic testcase are inserted here. +# Keys are: fail, result, proof, noproof (no proof generated when should), +# time, timeTooMuch, lang (wrong language), +# error (stp reported errors, but didn't die) +my %testsDB=(); + +# Search for a string element in the array ref, and return 1 if found, 0 if not +sub findStringElement { + my ($el, $aRef) = @_; + foreach my $v (@{$aRef}) { + if($v eq $el) { return 1; } + } + return 0; +} + +# Add a testcase to the set of problematic runs. +# Args: +# test is the full or relative path to the test file +# lang is the input language (not used currently) +# problem is the name of the problem the testcase exhibits +sub addProblem { + my ($test, $lang, $problem) = @_; + my $aRef = $testsDB{$problem}; + if(!defined($aRef)) { $aRef=[ ]; } + if(!findStringElement($test, $aRef)) { + $testsDB{$problem} = [@{$aRef}, $test]; + } +} + +# Total running time +my $totalTime = time; +my $defaultDir = `pwd`; +$defaultDir =~ s/\n//; + +foreach my $testcase (@testcases) { + chdir $defaultDir or die "Cannot chdir to $defaultDir: $?"; + my @testcasesTmp = (); + if(-f $testcase) { push @testcasesTmp, $testcase; } + elsif(-d $testcase) { + # Compute the list of files for testcases + opendir(TESTS, $testcase) + or die "Cannot open directory $testcase: $?"; + @testcasesTmp = grep { + /[.]([sc]vcl?|li?sp|smt)$/ && -f "$testcase/$_" } readdir(TESTS); + closedir TESTS; + @testcasesTmp = map { "$testcase/$_" } @testcasesTmp; + } else { + print("*** Error: WARNING: cannot find testcase $testcase: ", + "no such file or directory\n"); + } + + for(my $i=0; $i<=$#testcasesTmp; $i++) { + my $name = $testcasesTmp[$i]; + my $file = "$defaultDir/$name"; + my $hasProblem=0; + if(!(-f $file)) { + print "Error: WARNING: no such file: $file\n"; + next; + } + my %opt = getTestOpt($file); + # Check regression level + if(defined($opt{'level'}) && $level < $opt{'level'}) { + # Regression level of this test is too high; skip it + next; + } + # Print the testcase name + print("===============================================\n", + $testcasesTmp[$i], ":\n"); + # Check the input language + if($lang ne "all" && defined($opt{'lang'}) && $lang ne $opt{'lang'}) { + print "Error: Wrong input language, skipping $testcasesTmp[$i]\n"; + $hasProblem=1; + addProblem($name, $lang, 'lang'); + next; + } + my $checkProofs = getOpt('proofs', \%opt); + my $expRuntime = $opt{'runtime'}; + my $expResult = $opt{'result'}; + my $stpOptions = getOpt('stpOptions', \%opt); + # Print some testcase specific info + if($verbose) { + print("Language: $lang\n"); + print("Checking proofs: ", ($checkProofs)? "yes" : "no", + "\n"); + #if($rt && defined($expRuntime)) { + if(defined($expRuntime)) { + print("Expected runtime: ", $expRuntime, " sec\n"); + } + if(defined($expResult)) { + print("Expected result: ", $expResult, "\n"); + } + if($stpOptions =~ /\S/) { + print("STP options: ", $stpOptions, "\n"); + } + } + # Create a temporary dir, but first delete it; there may be + # junk there + system("/bin/rm -rf $tmpdir"); + mkdir $tmpdir or die "Cannot create directory $tmpdir: $?"; + chdir $tmpdir or die "Cannot chdir to $tmpdir: $?"; + + # Compute stp arguments + my @stpArgs = (); + # push @stpArgs, ($checkProofs)? "+proofs" : "-proofs"; + # if($lang ne "all") { push @stpArgs, "-lang $lang"; } + # push @stpArgs, $stpOptions; + # my $stpArgs = join(" ", @stpArgs); + # Now, run the sucker + my $timeMax = getOpt('time'); + my $timeLimit = ($timeMax > 0)? "-t $timeMax" : ""; + my $limits = "ulimit -c 0; ulimit -d 2000000; ulimit -m 2000000; ulimit -v 2000000; ulimit $timeLimit"; + # "-s 10240 -v 2000000 $timeLimit"; + my $logging = ($verbose)? " 2>&1 | tee output" : "> output 2>&1"; + my $timing = ($verbose)? "time " : ""; + if($verbose) { + print "***\n"; + #print "Running $stp $stpArgs < $file\n"; + print "Running $stp < $file\n"; + print "***\n"; + } + my $time = time; + # my $exitVal = system("$limits; $timing $stp $stpArgs " + my $exitVal = system("$limits; $timing $stp " + #my $exitVal = system("$timing $stp " + . "< $file $logging"); + $time = time - $time; + # OK, let's see what happened + $testsTotal++; + # Printing runtime + print "Runtime: $time sec"; + if($rt && defined($expRuntime)) { + if($time > $expRuntime) { + if($time > 10*$expRuntime) { + print " MUCH"; + addProblem($name, $lang, 'timeTooMuch'); + } + print " : LONGER than expected: $expRuntime sec"; + $hasProblem=1; + addProblem($name, $lang, 'time'); + } + elsif($expRuntime >= 5 && $time < $expRuntime/2) { + print " : much FASTER than expected: $expRuntime sec"; + addProblem($name, $lang, 'timeFast'); + $hasProblem=1; + } + } + print "\n"; + # Parsing the output + open IN, "output" or die "Cannot open `pwd`/output: $?"; + my $str; + my $result=""; + my $hasErrors=0; + while(defined($str=)) { + # Find at least one valid result + if($result ne "valid" && $str =~ /^(Valid|In[Vv]alid|Unknown)./) { + $result=lc $1; + } + # STP exit value may be masked by the shell pipe. Fish it + # out from the output + if($str =~ /^(Interrupted|Segmentation|Bus error|Floating point exception|.*exception)/) { + $exitVal = $1; + } + if($str =~ /^(\*|\s)*((parse\s+)?[Ee]rror)/) { + $hasErrors=1; + } + } + close IN; + if($exitVal ne "0") { + print "*** Error: STP FAILED with exit code $exitVal\n"; + $hasProblem=1; + addProblem($name, $lang, 'fail'); + } + # Checking for errors + if($hasErrors) { + $hasProblem=1; + addProblem($name, $lang, 'error'); + print "ERRORS in the test\n"; + } + # Printing result diagnostics + if(defined($expResult)) { + if($expResult ne $result) { + $hasProblem=1; + if($result eq "") { + addProblem($name, $lang, 'fail'); + print("Error: FAILED (no result, expected $expResult)\n"); + } else { + addProblem($name, $lang, 'result'); + print("Error: WRONG RESULT (", $result, + " instead of $expResult)\n"); + } + } else { + print "Result is correct\n"; + } + } + # else { +# print "Error: No result\n"; +# } + $testsProblems += $hasProblem; + print("=============== End of testcase ===============\n"); + } +} + +$totalTime = time - $totalTime; + +print "\nStatistics:\n"; +print "Total tests run: $testsTotal\n"; +print "Total running time: $totalTime sec\n"; +print "Total number of proofs checked: $proofsChecked\n"; +print "Problematic cases: $testsProblems\n"; +if($testsProblems > 0 && $verbose) { + my $aref; + print "\nDetailed Statistics:\n"; + $aref=$testsDB{'fail'}; + if(defined($aref)) { + my @a = @{$aref}; + printf("Failed tests [%d]:\n", $#a+1); + foreach my $n (@a) { print " $n\n"; } + } + $aref=$testsDB{'error'}; + if(defined($aref)) { + my @a = @{$aref}; + printf("Tests with errors [%d]:\n", $#a+1); + foreach my $n (@a) { print " $n\n"; } + } + $aref=$testsDB{'result'}; + if(defined($aref)) { + my @a = @{$aref}; + printf("Tests with wrong results [%d]:\n", $#a+1); + foreach my $n (@a) { print " $n\n"; } + } + $aref=$testsDB{'proof'}; + if(defined($aref)) { + my @a = @{$aref}; + printf("Tests with failed proofs [%d]:\n", $#a+1); + foreach my $n (@a) { print " $n\n"; } + } + $aref=$testsDB{'noproof'}; + if(defined($aref)) { + my @a = @{$aref}; + printf("Tests that should have proofs but don't [%d]:\n", $#a+1); + foreach my $n (@a) { print " $n\n"; } + } + $aref=$testsDB{'timeFast'}; + if(defined($aref)) { + my @a = @{$aref}; + printf("Tests running at least twice as fast as expected [%d]:\n", $#a+1); + foreach my $n (@a) { print " $n\n"; } + } + $aref=$testsDB{'time'}; + if(defined($aref)) { + my @a = @{$aref}; + printf("Tests running longer [%d]:\n", $#a+1); + foreach my $n (@a) { print " $n\n"; } + } + $aref=$testsDB{'timeTooMuch'}; + if(defined($aref)) { + my @a = @{$aref}; + printf("...including tests running WAY too long [%d]:\n", $#a+1); + foreach my $n (@a) { print " $n\n"; } + } + $aref=$testsDB{'lang'}; + if(defined($aref)) { + my @a = @{$aref}; + printf("Tests with wrong input language [%d]:\n", $#a+1); + foreach my $n (@a) { print " $n\n"; } + } +} + +# Delete temporary dir if there is one +system("/bin/rm -rf $tmpdir"); + +exit ($testsProblems > 0 ? 2 : 0); diff --git a/sat/core/Main.C b/sat/core/Main.C deleted file mode 100644 index acef32c..0000000 --- a/sat/core/Main.C +++ /dev/null @@ -1,344 +0,0 @@ -/******************************************************************************************[Main.C] -MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ - -#include -#include -#include -#include - -#include -#include - -#include "Solver.h" - -/*************************************************************************************/ -#ifdef _MSC_VER -#include - -static inline double cpuTime(void) { - return (double)clock() / CLOCKS_PER_SEC; } -#else - -#include -#include -#include - -static inline double cpuTime(void) { - struct rusage ru; - getrusage(RUSAGE_SELF, &ru); - return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; } -#endif - - -#if defined(__linux__) -static inline int memReadStat(int field) -{ - char name[256]; - pid_t pid = getpid(); - sprintf(name, "/proc/%d/statm", pid); - FILE* in = fopen(name, "rb"); - if (in == NULL) return 0; - int value; - for (; field >= 0; field--) - fscanf(in, "%d", &value); - fclose(in); - return value; -} -static inline uint64_t memUsed() { return (uint64_t)memReadStat(0) * (uint64_t)getpagesize(); } - - -#elif defined(__FreeBSD__) -static inline uint64_t memUsed(void) { - struct rusage ru; - getrusage(RUSAGE_SELF, &ru); - return ru.ru_maxrss*1024; } - - -#else -static inline uint64_t memUsed() { return 0; } -#endif - -#if defined(__linux__) -#include -#endif - -//================================================================================================= -// DIMACS Parser: - -#define CHUNK_LIMIT 1048576 - -class StreamBuffer { - gzFile in; - char buf[CHUNK_LIMIT]; - int pos; - int size; - - void assureLookahead() { - if (pos >= size) { - pos = 0; - size = gzread(in, buf, sizeof(buf)); } } - -public: - StreamBuffer(gzFile i) : in(i), pos(0), size(0) { - assureLookahead(); } - - int operator * () { return (pos >= size) ? EOF : buf[pos]; } - void operator ++ () { pos++; assureLookahead(); } -}; - -//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -template -static void skipWhitespace(B& in) { - while ((*in >= 9 && *in <= 13) || *in == 32) - ++in; } - -template -static void skipLine(B& in) { - for (;;){ - if (*in == EOF || *in == '\0') return; - if (*in == '\n') { ++in; return; } - ++in; } } - -template -static int parseInt(B& in) { - int val = 0; - bool neg = false; - skipWhitespace(in); - if (*in == '-') neg = true, ++in; - else if (*in == '+') ++in; - if (*in < '0' || *in > '9') reportf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3); - while (*in >= '0' && *in <= '9') - val = val*10 + (*in - '0'), - ++in; - return neg ? -val : val; } - -template -static void readClause(B& in, Solver& S, vec& lits) { - int parsed_lit, var; - lits.clear(); - for (;;){ - parsed_lit = parseInt(in); - if (parsed_lit == 0) break; - var = abs(parsed_lit)-1; - while (var >= S.nVars()) S.newVar(); - lits.push( (parsed_lit > 0) ? Lit(var) : ~Lit(var) ); - } -} - -template -static bool match(B& in, char* str) { - for (; *str != 0; ++str, ++in) - if (*str != *in) - return false; - return true; -} - - -template -static void parse_DIMACS_main(B& in, Solver& S) { - vec lits; - for (;;){ - skipWhitespace(in); - if (*in == EOF) - break; - else if (*in == 'p'){ - if (match(in, "p cnf")){ - int vars = parseInt(in); - int clauses = parseInt(in); - reportf("| Number of variables: %-12d |\n", vars); - reportf("| Number of clauses: %-12d |\n", clauses); - }else{ - reportf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3); - } - } else if (*in == 'c' || *in == 'p') - skipLine(in); - else - readClause(in, S, lits), - S.addClause(lits); - } -} - -// Inserts problem into solver. -// -static void parse_DIMACS(gzFile input_stream, Solver& S) { - StreamBuffer in(input_stream); - parse_DIMACS_main(in, S); } - - -//================================================================================================= - - -void printStats(Solver& solver) -{ - double cpu_time = cpuTime(); - uint64_t mem_used = memUsed(); - reportf("restarts : %lld\n", solver.starts); - reportf("conflicts : %-12lld (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); - reportf("decisions : %-12lld (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time); - reportf("propagations : %-12lld (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); - reportf("conflict literals : %-12lld (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); - if (mem_used != 0) reportf("Memory used : %.2f MB\n", mem_used / 1048576.0); - reportf("CPU time : %g s\n", cpu_time); -} - -Solver* solver; -static void SIGINT_handler(int signum) { - reportf("\n"); reportf("*** INTERRUPTED ***\n"); - printStats(*solver); - reportf("\n"); reportf("*** INTERRUPTED ***\n"); - exit(1); } - - -//================================================================================================= -// Main: - -void printUsage(char** argv) -{ - reportf("USAGE: %s [options] \n\n where input may be either in plain or gzipped DIMACS.\n\n", argv[0]); - reportf("OPTIONS:\n\n"); - reportf(" -polarity-mode = {true,false,rnd}\n"); - reportf(" -decay = [ 0 - 1 ]\n"); - reportf(" -rnd-freq = [ 0 - 1 ]\n"); - reportf(" -verbosity = {0,1,2}\n"); - reportf("\n"); -} - - -const char* hasPrefix(const char* str, const char* prefix) -{ - int len = strlen(prefix); - if (strncmp(str, prefix, len) == 0) - return str + len; - else - return NULL; -} - - -int main(int argc, char** argv) -{ - Solver S; - S.verbosity = 1; - - - int i, j; - const char* value; - for (i = j = 0; i < argc; i++){ - if ((value = hasPrefix(argv[i], "-polarity-mode="))){ - if (strcmp(value, "true") == 0) - S.polarity_mode = Solver::polarity_true; - else if (strcmp(value, "false") == 0) - S.polarity_mode = Solver::polarity_false; - else if (strcmp(value, "rnd") == 0) - S.polarity_mode = Solver::polarity_rnd; - else{ - reportf("ERROR! unknown polarity-mode %s\n", value); - exit(0); } - - }else if ((value = hasPrefix(argv[i], "-rnd-freq="))){ - double rnd; - if (sscanf(value, "%lf", &rnd) <= 0 || rnd < 0 || rnd > 1){ - reportf("ERROR! illegal rnd-freq constant %s\n", value); - exit(0); } - S.random_var_freq = rnd; - - }else if ((value = hasPrefix(argv[i], "-decay="))){ - double decay; - if (sscanf(value, "%lf", &decay) <= 0 || decay <= 0 || decay > 1){ - reportf("ERROR! illegal decay constant %s\n", value); - exit(0); } - S.var_decay = 1 / decay; - - }else if ((value = hasPrefix(argv[i], "-verbosity="))){ - int verbosity = (int)strtol(value, NULL, 10); - if (verbosity == 0 && errno == EINVAL){ - reportf("ERROR! illegal verbosity level %s\n", value); - exit(0); } - S.verbosity = verbosity; - - }else if (strcmp(argv[i], "-h") == 0 || strcmp(argv[i], "-help") == 0 || strcmp(argv[i], "--help") == 0){ - printUsage(argv); - exit(0); - - }else if (strncmp(argv[i], "-", 1) == 0){ - reportf("ERROR! unknown flag %s\n", argv[i]); - exit(0); - - }else - argv[j++] = argv[i]; - } - argc = j; - - - reportf("This is MiniSat 2.0 beta\n"); -#if defined(__linux__) - fpu_control_t oldcw, newcw; - _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw); - reportf("WARNING: for repeatability, setting FPU to use double precision\n"); -#endif - double cpu_time = cpuTime(); - - solver = &S; - signal(SIGINT,SIGINT_handler); - signal(SIGHUP,SIGINT_handler); - - if (argc == 1) - reportf("Reading from standard input... Use '-h' or '--help' for help.\n"); - - gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb"); - if (in == NULL) - reportf("ERROR! Could not open file: %s\n", argc == 1 ? "" : argv[1]), exit(1); - - reportf("============================[ Problem Statistics ]=============================\n"); - reportf("| |\n"); - - parse_DIMACS(in, S); - gzclose(in); - FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL; - - double parse_time = cpuTime() - cpu_time; - reportf("| Parsing time: %-12.2f s |\n", parse_time); - - if (!S.simplify()){ - reportf("Solved by unit propagation\n"); - if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res); - printf("UNSATISFIABLE\n"); - exit(20); - } - - bool ret = S.solve(); - printStats(S); - reportf("\n"); - printf(ret ? "SATISFIABLE\n" : "UNSATISFIABLE\n"); - if (res != NULL){ - if (ret){ - fprintf(res, "SAT\n"); - for (int i = 0; i < S.nVars(); i++) - if (S.model[i] != l_Undef) - fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); - fprintf(res, " 0\n"); - }else - fprintf(res, "UNSAT\n"); - fclose(res); - } - -#ifdef NDEBUG - exit(ret ? 10 : 20); // (faster than "return", which will invoke the destructor for 'Solver') -#endif -} diff --git a/sat/core/Makefile b/sat/core/Makefile index 076ad6d..ea85050 100644 --- a/sat/core/Makefile +++ b/sat/core/Makefile @@ -4,4 +4,7 @@ EXEC = minisat CFLAGS = -I$(MTL) -Wall -DEXT_HASH_MAP -ffloat-store LFLAGS = -lz + include ../mtl/template.mk +all: + cp libminisat.a ../ \ No newline at end of file diff --git a/sat/mtl/template.mk b/sat/mtl/template.mk index d894d74..e60f2fb 100644 --- a/sat/mtl/template.mk +++ b/sat/mtl/template.mk @@ -76,7 +76,7 @@ lib$(LIB).a lib$(LIB)d.a lib$(LIB)p.a: ## Clean rule clean: - @rm -f $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \ + @rm -f *~ $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \ $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) *.core depend.mak lib$(LIB).a lib$(LIB)d.a lib$(LIB)p.a ## Make dependencies diff --git a/sat/simp/Main.C b/sat/simp/Main.C deleted file mode 100644 index b6d1946..0000000 --- a/sat/simp/Main.C +++ /dev/null @@ -1,415 +0,0 @@ -/******************************************************************************************[Main.C] -MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ - -#include -#include -#include -#include - -#include -#include - -#include "SimpSolver.h" - -/*************************************************************************************/ -#ifdef _MSC_VER -#include - -static inline double cpuTime(void) { - return (double)clock() / CLOCKS_PER_SEC; } -#else - -#include -#include -#include - -static inline double cpuTime(void) { - struct rusage ru; - getrusage(RUSAGE_SELF, &ru); - return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; } -#endif - - -#if defined(__linux__) -static inline int memReadStat(int field) -{ - char name[256]; - pid_t pid = getpid(); - sprintf(name, "/proc/%d/statm", pid); - FILE* in = fopen(name, "rb"); - if (in == NULL) return 0; - int value; - for (; field >= 0; field--) - fscanf(in, "%d", &value); - fclose(in); - return value; -} -static inline uint64_t memUsed() { return (uint64_t)memReadStat(0) * (uint64_t)getpagesize(); } - - -#elif defined(__FreeBSD__) -static inline uint64_t memUsed(void) { - struct rusage ru; - getrusage(RUSAGE_SELF, &ru); - return ru.ru_maxrss*1024; } - - -#else -static inline uint64_t memUsed() { return 0; } -#endif - -#if defined(__linux__) -#include -#endif - - -//================================================================================================= -// DIMACS Parser: - -#define CHUNK_LIMIT 1048576 - -class StreamBuffer { - gzFile in; - char buf[CHUNK_LIMIT]; - int pos; - int size; - - void assureLookahead() { - if (pos >= size) { - pos = 0; - size = gzread(in, buf, sizeof(buf)); } } - -public: - StreamBuffer(gzFile i) : in(i), pos(0), size(0) { - assureLookahead(); } - - int operator * () { return (pos >= size) ? EOF : buf[pos]; } - void operator ++ () { pos++; assureLookahead(); } -}; - -//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -template -static void skipWhitespace(B& in) { - while ((*in >= 9 && *in <= 13) || *in == 32) - ++in; } - -template -static void skipLine(B& in) { - for (;;){ - if (*in == EOF || *in == '\0') return; - if (*in == '\n') { ++in; return; } - ++in; } } - -template -static int parseInt(B& in) { - int val = 0; - bool neg = false; - skipWhitespace(in); - if (*in == '-') neg = true, ++in; - else if (*in == '+') ++in; - if (*in < '0' || *in > '9') reportf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3); - while (*in >= '0' && *in <= '9') - val = val*10 + (*in - '0'), - ++in; - return neg ? -val : val; } - -template -static void readClause(B& in, SimpSolver& S, vec& lits) { - int parsed_lit, var; - lits.clear(); - for (;;){ - parsed_lit = parseInt(in); - if (parsed_lit == 0) break; - var = abs(parsed_lit)-1; - while (var >= S.nVars()) S.newVar(); - lits.push( (parsed_lit > 0) ? Lit(var) : ~Lit(var) ); - } -} - -template -static bool match(B& in, char* str) { - for (; *str != 0; ++str, ++in) - if (*str != *in) - return false; - return true; -} - - -template -static void parse_DIMACS_main(B& in, SimpSolver& S) { - vec lits; - for (;;){ - skipWhitespace(in); - if (*in == EOF) break; - else if (*in == 'p'){ - if (match(in, "p cnf")){ - int vars = parseInt(in); - int clauses = parseInt(in); - reportf("| Number of variables: %-12d |\n", vars); - reportf("| Number of clauses: %-12d |\n", clauses); - - // SATRACE'06 hack - if (clauses > 4000000) - S.eliminate(true); - }else{ - reportf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3); - } - } else if (*in == 'c' || *in == 'p') - skipLine(in); - else{ - readClause(in, S, lits); - S.addClause(lits); } - } -} - -// Inserts problem into solver. -// -static void parse_DIMACS(gzFile input_stream, SimpSolver& S) { - StreamBuffer in(input_stream); - parse_DIMACS_main(in, S); } - - -//================================================================================================= - - -void printStats(Solver& S) -{ - double cpu_time = cpuTime(); - uint64_t mem_used = memUsed(); - reportf("restarts : %lld\n", S.starts); - reportf("conflicts : %-12lld (%.0f /sec)\n", S.conflicts , S.conflicts /cpu_time); - reportf("decisions : %-12lld (%4.2f %% random) (%.0f /sec)\n", S.decisions, (float)S.rnd_decisions*100 / (float)S.decisions, S.decisions /cpu_time); - reportf("propagations : %-12lld (%.0f /sec)\n", S.propagations, S.propagations/cpu_time); - reportf("conflict literals : %-12lld (%4.2f %% deleted)\n", S.tot_literals, (S.max_literals - S.tot_literals)*100 / (double)S.max_literals); - if (mem_used != 0) reportf("Memory used : %.2f MB\n", mem_used / 1048576.0); - reportf("CPU time : %g s\n", cpu_time); -} - -SimpSolver* solver; -static void SIGINT_handler(int signum) { - reportf("\n"); reportf("*** INTERRUPTED ***\n"); - printStats(*solver); - reportf("\n"); reportf("*** INTERRUPTED ***\n"); - exit(1); } - - -//================================================================================================= -// Main: - -void printUsage(char** argv) -{ - reportf("USAGE: %s [options] \n\n where input may be either in plain or gzipped DIMACS.\n\n", argv[0]); - reportf("OPTIONS:\n\n"); - reportf(" -pre = {none,once}\n"); - reportf(" -asymm\n"); - reportf(" -rcheck\n"); - reportf(" -grow = [ >0 ]\n"); - reportf(" -polarity-mode = {true,false,rnd}\n"); - reportf(" -decay = [ 0 - 1 ]\n"); - reportf(" -rnd-freq = [ 0 - 1 ]\n"); - reportf(" -dimacs = \n"); - reportf(" -verbosity = {0,1,2}\n"); - reportf("\n"); -} - -typedef enum { pre_none, pre_once, pre_repeat } preprocessMode; - -const char* hasPrefix(const char* str, const char* prefix) -{ - int len = strlen(prefix); - if (strncmp(str, prefix, len) == 0) - return str + len; - else - return NULL; -} - - -int main(int argc, char** argv) -{ - reportf("This is MiniSat 2.0 beta\n"); -#if defined(__linux__) - fpu_control_t oldcw, newcw; - _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw); - reportf("WARNING: for repeatability, setting FPU to use double precision\n"); -#endif - preprocessMode pre = pre_once; - const char* dimacs = NULL; - const char* freeze = NULL; - SimpSolver S; - S.verbosity = 1; - - // This just grew and grew, and I didn't have time to do sensible argument parsing yet :) - // - int i, j; - const char* value; - for (i = j = 0; i < argc; i++){ - if ((value = hasPrefix(argv[i], "-polarity-mode="))){ - if (strcmp(value, "true") == 0) - S.polarity_mode = Solver::polarity_true; - else if (strcmp(value, "false") == 0) - S.polarity_mode = Solver::polarity_false; - else if (strcmp(value, "rnd") == 0) - S.polarity_mode = Solver::polarity_rnd; - else{ - reportf("ERROR! unknown polarity-mode %s\n", value); - exit(0); } - - }else if ((value = hasPrefix(argv[i], "-rnd-freq="))){ - double rnd; - if (sscanf(value, "%lf", &rnd) <= 0 || rnd < 0 || rnd > 1){ - reportf("ERROR! illegal rnd-freq constant %s\n", value); - exit(0); } - S.random_var_freq = rnd; - - }else if ((value = hasPrefix(argv[i], "-decay="))){ - double decay; - if (sscanf(value, "%lf", &decay) <= 0 || decay <= 0 || decay > 1){ - reportf("ERROR! illegal decay constant %s\n", value); - exit(0); } - S.var_decay = 1 / decay; - - }else if ((value = hasPrefix(argv[i], "-verbosity="))){ - int verbosity = (int)strtol(value, NULL, 10); - if (verbosity == 0 && errno == EINVAL){ - reportf("ERROR! illegal verbosity level %s\n", value); - exit(0); } - S.verbosity = verbosity; - - }else if ((value = hasPrefix(argv[i], "-pre="))){ - if (strcmp(value, "none") == 0) - pre = pre_none; - else if (strcmp(value, "once") == 0) - pre = pre_once; - else if (strcmp(value, "repeat") == 0){ - pre = pre_repeat; - reportf("ERROR! preprocessing mode \"repeat\" is not supported at the moment.\n"); - exit(0); - }else{ - reportf("ERROR! unknown preprocessing mode %s\n", value); - exit(0); } - }else if (strcmp(argv[i], "-asymm") == 0){ - S.asymm_mode = true; - }else if (strcmp(argv[i], "-rcheck") == 0){ - S.redundancy_check = true; - }else if ((value = hasPrefix(argv[i], "-grow="))){ - int grow = (int)strtol(value, NULL, 10); - if (grow == 0 && errno == EINVAL){ - reportf("ERROR! illegal grow constant %s\n", &argv[i][6]); - exit(0); } - S.grow = grow; - }else if ((value = hasPrefix(argv[i], "-dimacs="))){ - dimacs = value; - }else if ((value = hasPrefix(argv[i], "-freeze="))){ - freeze = value; - }else if (strcmp(argv[i], "-h") == 0 || strcmp(argv[i], "-help") == 0){ - printUsage(argv); - exit(0); - }else if (strncmp(argv[i], "-", 1) == 0){ - reportf("ERROR! unknown flag %s\n", argv[i]); - exit(0); - }else - argv[j++] = argv[i]; - } - argc = j; - - double cpu_time = cpuTime(); - - if (pre == pre_none) - S.eliminate(true); - - solver = &S; - signal(SIGINT,SIGINT_handler); - signal(SIGHUP,SIGINT_handler); - - if (argc == 1) - reportf("Reading from standard input... Use '-h' or '--help' for help.\n"); - - gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb"); - if (in == NULL) - reportf("ERROR! Could not open file: %s\n", argc == 1 ? "" : argv[1]), exit(1); - - reportf("============================[ Problem Statistics ]=============================\n"); - reportf("| |\n"); - - parse_DIMACS(in, S); - gzclose(in); - FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL; - - - double parse_time = cpuTime() - cpu_time; - reportf("| Parsing time: %-12.2f s |\n", parse_time); - - /*HACK: Freeze variables*/ - if (freeze != NULL && pre != pre_none){ - int count = 0; - FILE* in = fopen(freeze, "rb"); - for(;;){ - Var x; - fscanf(in, "%d", &x); - if (x == 0) break; - x--; - - /**/assert(S.n_occ[toInt(Lit(x))] + S.n_occ[toInt(~Lit(x))] != 0); - /**/assert(S.value(x) == l_Undef); - S.setFrozen(x, true); - count++; - } - fclose(in); - reportf("| Frozen vars : %-12.0f |\n", (double)count); - } - /*END*/ - - if (!S.simplify()){ - reportf("Solved by unit propagation\n"); - if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res); - printf("UNSATISFIABLE\n"); - exit(20); - } - - if (dimacs){ - if (pre != pre_none) - S.eliminate(true); - reportf("==============================[ Writing DIMACS ]===============================\n"); - S.toDimacs(dimacs); - printStats(S); - exit(0); - }else{ - bool ret = S.solve(true, true); - printStats(S); - reportf("\n"); - - printf(ret ? "SATISFIABLE\n" : "UNSATISFIABLE\n"); - if (res != NULL){ - if (ret){ - fprintf(res, "SAT\n"); - for (int i = 0; i < S.nVars(); i++) - if (S.model[i] != l_Undef) - fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); - fprintf(res, " 0\n"); - }else - fprintf(res, "UNSAT\n"); - fclose(res); - } -#ifdef NDEBUG - exit(ret ? 10 : 20); // (faster than "return", which will invoke the destructor for 'Solver') -#endif - } - -} diff --git a/sat/simp/Makefile b/sat/simp/Makefile index f543982..26974d1 100644 --- a/sat/simp/Makefile +++ b/sat/simp/Makefile @@ -9,3 +9,5 @@ CSRCS = $(wildcard *.C) COBJS = $(addsuffix .o, $(basename $(CSRCS))) $(CORE)/Solver.o include ../mtl/template.mk +all: + cp libminisat.a ../ \ No newline at end of file diff --git a/sat/simp/SimpSolver.h b/sat/simp/SimpSolver.h index 8135e43..ea05f85 100644 --- a/sat/simp/SimpSolver.h +++ b/sat/simp/SimpSolver.h @@ -29,51 +29,51 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA namespace MINISAT { /*************************************************************************************/ -#ifdef _MSC_VER -#include - -static inline double cpuTime(void) { - return (double)clock() / CLOCKS_PER_SEC; } -#else - -#include -#include -#include - -static inline double cpuTime(void) { - struct rusage ru; - getrusage(RUSAGE_SELF, &ru); - return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; } -#endif - - -#if defined(__linux__) -static inline int memReadStat(int field) -{ - char name[256]; - pid_t pid = getpid(); - sprintf(name, "/proc/%d/statm", pid); - FILE* in = fopen(name, "rb"); - if (in == NULL) return 0; - int value; - for (; field >= 0; field--) - fscanf(in, "%d", &value); - fclose(in); - return value; -} -static inline uint64_t memUsed() { return (uint64_t)memReadStat(0) * (uint64_t)getpagesize(); } - - -#elif defined(__FreeBSD__) -static inline uint64_t memUsed(void) { - struct rusage ru; - getrusage(RUSAGE_SELF, &ru); - return ru.ru_maxrss*1024; } - - -#else -static inline uint64_t memUsed() { return 0; } -#endif +/* #ifdef _MSC_VER */ +/* #include */ + +/* static inline double cpuTime(void) { */ +/* return (double)clock() / CLOCKS_PER_SEC; } */ +/* #else */ + +/* #include */ +/* #include */ +/* #include */ + +/* static inline double cpuTime(void) { */ +/* struct rusage ru; */ +/* getrusage(RUSAGE_SELF, &ru); */ +/* return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; } */ +/* #endif */ + + +/* #if defined(__linux__) */ +/* static inline int memReadStat(int field) */ +/* { */ +/* char name[256]; */ +/* pid_t pid = getpid(); */ +/* sprintf(name, "/proc/%d/statm", pid); */ +/* FILE* in = fopen(name, "rb"); */ +/* if (in == NULL) return 0; */ +/* int value; */ +/* for (; field >= 0; field--) */ +/* fscanf(in, "%d", &value); */ +/* fclose(in); */ +/* return value; */ +/* } */ +/* static inline uint64_t memUsed() { return (uint64_t)memReadStat(0) * (uint64_t)getpagesize(); } */ + + +/* #elif defined(__FreeBSD__) */ +/* static inline uint64_t memUsed(void) { */ +/* struct rusage ru; */ +/* getrusage(RUSAGE_SELF, &ru); */ +/* return ru.ru_maxrss*1024; } */ + + +/* #else */ +/* static inline uint64_t memUsed() { return 0; } */ +/* #endif */ #if defined(__linux__) #include diff --git a/sat/simp/depend.mk b/sat/simp/depend.mk index c5d74f8..cd452e0 100644 --- a/sat/simp/depend.mk +++ b/sat/simp/depend.mk @@ -1,20 +1,24 @@ Main.o: Main.C SimpSolver.h ../mtl/Queue.h ../mtl/Vec.h ../core/Solver.h \ - ../mtl/Map.h ../mtl/Heap.h ../mtl/Alg.h ../core/SolverTypes.h -SimpSolver.o: SimpSolver.C ../mtl/Sort.h ../mtl/Vec.h SimpSolver.h \ - ../mtl/Queue.h ../core/Solver.h ../mtl/Map.h ../mtl/Heap.h ../mtl/Alg.h \ + ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h ../mtl/Alg.h \ ../core/SolverTypes.h +SimpSolver.o: SimpSolver.C ../mtl/Sort.h ../mtl/Vec.h SimpSolver.h \ + ../mtl/Queue.h ../core/Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \ + ../mtl/Alg.h ../core/SolverTypes.h Main.op: Main.C SimpSolver.h ../mtl/Queue.h ../mtl/Vec.h ../core/Solver.h \ - ../mtl/Map.h ../mtl/Heap.h ../mtl/Alg.h ../core/SolverTypes.h -SimpSolver.op: SimpSolver.C ../mtl/Sort.h ../mtl/Vec.h SimpSolver.h \ - ../mtl/Queue.h ../core/Solver.h ../mtl/Map.h ../mtl/Heap.h ../mtl/Alg.h \ + ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h ../mtl/Alg.h \ ../core/SolverTypes.h +SimpSolver.op: SimpSolver.C ../mtl/Sort.h ../mtl/Vec.h SimpSolver.h \ + ../mtl/Queue.h ../core/Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \ + ../mtl/Alg.h ../core/SolverTypes.h Main.od: Main.C SimpSolver.h ../mtl/Queue.h ../mtl/Vec.h ../core/Solver.h \ - ../mtl/Map.h ../mtl/Heap.h ../mtl/Alg.h ../core/SolverTypes.h -SimpSolver.od: SimpSolver.C ../mtl/Sort.h ../mtl/Vec.h SimpSolver.h \ - ../mtl/Queue.h ../core/Solver.h ../mtl/Map.h ../mtl/Heap.h ../mtl/Alg.h \ + ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h ../mtl/Alg.h \ ../core/SolverTypes.h +SimpSolver.od: SimpSolver.C ../mtl/Sort.h ../mtl/Vec.h SimpSolver.h \ + ../mtl/Queue.h ../core/Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \ + ../mtl/Alg.h ../core/SolverTypes.h Main.or: Main.C SimpSolver.h ../mtl/Queue.h ../mtl/Vec.h ../core/Solver.h \ - ../mtl/Map.h ../mtl/Heap.h ../mtl/Alg.h ../core/SolverTypes.h -SimpSolver.or: SimpSolver.C ../mtl/Sort.h ../mtl/Vec.h SimpSolver.h \ - ../mtl/Queue.h ../core/Solver.h ../mtl/Map.h ../mtl/Heap.h ../mtl/Alg.h \ + ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h ../mtl/Alg.h \ ../core/SolverTypes.h +SimpSolver.or: SimpSolver.C ../mtl/Sort.h ../mtl/Vec.h SimpSolver.h \ + ../mtl/Queue.h ../core/Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \ + ../mtl/Alg.h ../core/SolverTypes.h -- 2.47.3