#include <algorithm>
#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 <stdlib.h>
#ifndef NATIVE_C_ARITH
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);
.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/
#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
--- /dev/null
+#!/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 = <IN>;
+ defined($str) && $lines > 0;
+ $lines--, $str = <IN>)
+ {
+ 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=<IN>)) {
+ # 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);
+++ /dev/null
-/******************************************************************************************[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 <ctime>
-#include <cstring>
-#include <stdint.h>
-#include <errno.h>
-
-#include <signal.h>
-#include <zlib.h>
-
-#include "Solver.h"
-
-/*************************************************************************************/
-#ifdef _MSC_VER
-#include <ctime>
-
-static inline double cpuTime(void) {
- return (double)clock() / CLOCKS_PER_SEC; }
-#else
-
-#include <sys/time.h>
-#include <sys/resource.h>
-#include <unistd.h>
-
-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 <fpu_control.h>
-#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<class B>
-static void skipWhitespace(B& in) {
- while ((*in >= 9 && *in <= 13) || *in == 32)
- ++in; }
-
-template<class B>
-static void skipLine(B& in) {
- for (;;){
- if (*in == EOF || *in == '\0') return;
- if (*in == '\n') { ++in; return; }
- ++in; } }
-
-template<class B>
-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<class B>
-static void readClause(B& in, Solver& S, vec<Lit>& 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<class B>
-static bool match(B& in, char* str) {
- for (; *str != 0; ++str, ++in)
- if (*str != *in)
- return false;
- return true;
-}
-
-
-template<class B>
-static void parse_DIMACS_main(B& in, Solver& S) {
- vec<Lit> 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] <input-file> <result-output-file>\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 = <num> [ 0 - 1 ]\n");
- reportf(" -rnd-freq = <num> [ 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 ? "<stdin>" : 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
-}
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
## 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
+++ /dev/null
-/******************************************************************************************[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 <ctime>
-#include <cstring>
-#include <stdint.h>
-#include <errno.h>
-
-#include <signal.h>
-#include <zlib.h>
-
-#include "SimpSolver.h"
-
-/*************************************************************************************/
-#ifdef _MSC_VER
-#include <ctime>
-
-static inline double cpuTime(void) {
- return (double)clock() / CLOCKS_PER_SEC; }
-#else
-
-#include <sys/time.h>
-#include <sys/resource.h>
-#include <unistd.h>
-
-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 <fpu_control.h>
-#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<class B>
-static void skipWhitespace(B& in) {
- while ((*in >= 9 && *in <= 13) || *in == 32)
- ++in; }
-
-template<class B>
-static void skipLine(B& in) {
- for (;;){
- if (*in == EOF || *in == '\0') return;
- if (*in == '\n') { ++in; return; }
- ++in; } }
-
-template<class B>
-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<class B>
-static void readClause(B& in, SimpSolver& S, vec<Lit>& 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<class B>
-static bool match(B& in, char* str) {
- for (; *str != 0; ++str, ++in)
- if (*str != *in)
- return false;
- return true;
-}
-
-
-template<class B>
-static void parse_DIMACS_main(B& in, SimpSolver& S) {
- vec<Lit> 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] <input-file> <result-output-file>\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 = <num> [ >0 ]\n");
- reportf(" -polarity-mode = {true,false,rnd}\n");
- reportf(" -decay = <num> [ 0 - 1 ]\n");
- reportf(" -rnd-freq = <num> [ 0 - 1 ]\n");
- reportf(" -dimacs = <output-file>\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 ? "<stdin>" : 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
- }
-
-}
COBJS = $(addsuffix .o, $(basename $(CSRCS))) $(CORE)/Solver.o
include ../mtl/template.mk
+all:
+ cp libminisat.a ../
\ No newline at end of file
namespace MINISAT {
/*************************************************************************************/
-#ifdef _MSC_VER
-#include <ctime>
-
-static inline double cpuTime(void) {
- return (double)clock() / CLOCKS_PER_SEC; }
-#else
-
-#include <sys/time.h>
-#include <sys/resource.h>
-#include <unistd.h>
-
-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 <ctime> */
+
+/* static inline double cpuTime(void) { */
+/* return (double)clock() / CLOCKS_PER_SEC; } */
+/* #else */
+
+/* #include <sys/time.h> */
+/* #include <sys/resource.h> */
+/* #include <unistd.h> */
+
+/* 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 <fpu_control.h>
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
projects / francis / stp.git / commitdiff