From: vijay_ganesh Date: Tue, 22 Sep 2009 00:43:54 +0000 (+0000) Subject: added new testing perl script. minor edits to Makefiles. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=33e382180b4271f9a9c61e23dc30517f2bb70aec;p=francis%2Fstp.git added new testing perl script. minor edits to Makefiles. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@247 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/Makefile b/Makefile index ad6a82a..98832fc 100644 --- a/Makefile +++ b/Makefile @@ -71,10 +71,7 @@ clean: .PHONY: regressall regressall: - $(MAKE) regresscvc - $(MAKE) regresssmt - $(MAKE) regresscapi - $(MAKE) regressbigarray + $(MAKE) regresscapi && $(MAKE) regresscvc && $(MAKE) regresssmt && $(MAKE) regressstp && $(MAKE) regressbigarray # The higher the level, the more tests are run (3 = all) REGRESS_LEVEL=4 @@ -146,6 +143,22 @@ regresscapi: @echo "*********************************************************" \ | tee -a $(CAPI_LOG) +STP_LOG = `date +%Y-%m-%d`"-regress-stp.log" +.PHONY: regressstp +regressstp: + @echo "*********************************************************" \ + | tee -a $(STP_LOG) + @echo "Starting tests at" `date` | tee -a $(STP_LOG) + @echo "*********************************************************" \ + | tee -a $(STP_LOG) + scripts/run_stp_tests.pl 2>&1 | tee -a $(STP_LOG); [ $${PIPESTATUS[0]} -eq 0 ] + @echo "*********************************************************" \ + | tee -a $(STP_LOG) + @echo "Output is saved in $(STP_LOG)" | tee -a $(STP_LOG) + @echo "*********************************************************" \ + | tee -a $(STP_LOG) + + GRIND_LOG = `date +%Y-%m-%d`"-grind.log" GRINDPROG = valgrind --leak-check=full --undef-value-errors=no GRIND_TAR = $(BIN_DIR)/stp -d diff --git a/README b/README index b38ba11..4794a20 100644 --- a/README +++ b/README @@ -50,5 +50,5 @@ make regresssmt make regresscvc make regresscapi make regressbigarray +make regressstp make regressall - diff --git a/scripts/Makefile.in b/scripts/Makefile.in index ad6a82a..98832fc 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -71,10 +71,7 @@ clean: .PHONY: regressall regressall: - $(MAKE) regresscvc - $(MAKE) regresssmt - $(MAKE) regresscapi - $(MAKE) regressbigarray + $(MAKE) regresscapi && $(MAKE) regresscvc && $(MAKE) regresssmt && $(MAKE) regressstp && $(MAKE) regressbigarray # The higher the level, the more tests are run (3 = all) REGRESS_LEVEL=4 @@ -146,6 +143,22 @@ regresscapi: @echo "*********************************************************" \ | tee -a $(CAPI_LOG) +STP_LOG = `date +%Y-%m-%d`"-regress-stp.log" +.PHONY: regressstp +regressstp: + @echo "*********************************************************" \ + | tee -a $(STP_LOG) + @echo "Starting tests at" `date` | tee -a $(STP_LOG) + @echo "*********************************************************" \ + | tee -a $(STP_LOG) + scripts/run_stp_tests.pl 2>&1 | tee -a $(STP_LOG); [ $${PIPESTATUS[0]} -eq 0 ] + @echo "*********************************************************" \ + | tee -a $(STP_LOG) + @echo "Output is saved in $(STP_LOG)" | tee -a $(STP_LOG) + @echo "*********************************************************" \ + | tee -a $(STP_LOG) + + GRIND_LOG = `date +%Y-%m-%d`"-grind.log" GRINDPROG = valgrind --leak-check=full --undef-value-errors=no GRIND_TAR = $(BIN_DIR)/stp -d diff --git a/scripts/run_stp_tests.pl b/scripts/run_stp_tests.pl new file mode 100755 index 0000000..4aed013 --- /dev/null +++ b/scripts/run_stp_tests.pl @@ -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 = ("tests/bio-tests", "tests/histar-big-tests", "tests/big-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/src/abstraction-refinement/AbstractionRefinement.cpp b/src/abstraction-refinement/AbstractionRefinement.cpp index b8bdea9..de8c3c1 100644 --- a/src/abstraction-refinement/AbstractionRefinement.cpp +++ b/src/abstraction-refinement/AbstractionRefinement.cpp @@ -265,7 +265,7 @@ namespace BEEV BeevMgr::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver, const ASTNode& original_input) { - cout << "The number of abs-refinement limit is " << num_absrefine << endl; + //cout << "The number of abs-refinement limit is " << num_absrefine << endl; for(int absrefine_count=0;absrefine_count < num_absrefine; absrefine_count++) { ASTVec Allretvec0; @@ -630,209 +630,5 @@ namespace BEEV ASTNodeMap ParamToCurrentValMap; return Check_FiniteLoop_UsingModel(finiteloop, &ParamToCurrentValMap, true); - } //end of Check_FiniteLoop_UsingModel - - -// /****************************************************************** -// * FINITE FORLOOP ABSTRACTION REFINEMENT -// * -// * For each 'finiteloop' in the list 'GlobalList_Of_FiniteLoops' -// * -// * Expand_FiniteLoop(finiteloop); -// * -// * The 'Expand_FiniteLoop' function expands the 'finiteloop' in a -// * counterexample-guided refinement fashion -// * -// * Once all the finiteloops have been expanded, we need to go back -// * and recheck that every discarded constraint is true with the -// * final model. A flag 'done' is set to false if atleast one -// * constraint is false during model-check, and is set to true if all -// * constraints are true during model-check. -// * -// * if the 'done' flag is true, then we terminate this refinement -// * loop. -// *****************************************************************/ - - -// SOLVER_RETURN_TYPE -// BeevMgr::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver, -// const ASTNode& original_input) -// { -// SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED; -// //cout << "The number of abs-refinement limit is " << num_absrefine << endl; -// for(int absrefine_count=0;absrefine_count < num_absrefine; absrefine_count++) -// { -// ASTVec Allretvec0; -// Allretvec0.push_back(ASTTrue); -// for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(), -// iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++) -// { - -// ASTNodeMap ParamToCurrentValMap; -// res = SATBased_FiniteLoop_Refinement(SatSolver, -// original_input, -// *i, -// &ParamToCurrentValMap, -// true); //absrefine flag -// if(SOLVER_UNDECIDED) -// { -// return res; -// } -// } //End of For -// } //end of absrefine count - -// res = SOLVER_UNDECIDED; -// for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(), -// iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++) -// { -// //cout << "The abs-refine didn't finish the job. Add the remaining formulas\n"; -// ASTNodeMap ParamToCurrentValMap; -// res = SATBased_FiniteLoop_Refinement(SatSolver, -// original_input, -// *i, -// &ParamToCurrentValMap, -// false); //absrefine flag -// if(SOLVER_UNDECIDED) -// { -// return res; -// } -// } //End of For - -// return res; -// } //end of SATBased_AllFiniteLoops_Refinement() - - -// /***************************************************************** -// * SATBased_FiniteLoop_Refinement -// * -// * 'finiteloop' is the finite loop to be expanded -// * Every finiteloop has three parts: -// * 0) Parameter Name -// * 1) Parameter initialization -// * 2) Parameter limit value -// * 3) Increment formula -// * 4) Formula Body -// * -// * ParamToCurrentValMap contains a map from parameters to their -// * current values in the recursion -// * -// * Nested FORs are allowed, but only the innermost loop can have a -// * formula in it -// *****************************************************************/ -// //SATBased_FiniteLoop_Refinement -// // -// //Expand the finite loop, check against model, and add false -// //formulas to the SAT solver -// SOLVER_RETURN_TYPE -// BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, -// const ASTNode& original_input, -// const ASTNode& finiteloop, -// ASTNodeMap* ParamToCurrentValMap, -// bool absrefine_flag) -// { -// //BVTypeCheck should have already checked the sanity of the input -// //FOR-formula -// ASTNode parameter = finiteloop[0]; -// int paramInit = GetUnsignedConst(finiteloop[1]); -// int paramLimit = GetUnsignedConst(finiteloop[2]); -// int paramIncrement = GetUnsignedConst(finiteloop[3]); -// ASTNode exceptFormula = finiteloop[4]; -// ASTNode formulabody = finiteloop[5]; -// int paramCurrentValue = paramInit; -// SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED; - -// //Update ParamToCurrentValMap with parameter and its current -// //value. Here paramCurrentValue is the initial value -// (*ParamToCurrentValMap)[parameter] = -// CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue); - -// //Go recursively thru' all the FOR-constructs. -// if(FOR == formulabody.GetKind()) -// { -// ASTVec retvec; -// ASTVec retvec_innerfor; -// retvec.push_back(ASTTrue); -// while(paramCurrentValue < paramLimit) -// { -// res = -// SATBased_FiniteLoop_Refinement(SatSolver, -// original_input, -// formulabody, -// ParamToCurrentValMap, -// absrefine_flag); - -// if(SOLVER_UNDECIDED != res) -// { -// return res; -// } - -// //Update ParamToCurrentValMap with parameter and its -// //current value. FIXME: Possible leak since I am not -// //freeing the previous 'value' for the same 'key' -// paramCurrentValue = paramCurrentValue + paramIncrement; -// (*ParamToCurrentValMap)[parameter] = -// CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue); -// } //end of While - -// return res; -// } //end of recursion FORs - -// //Expand the leaf level FOR-construct completely -// //increment of paramCurrentValue done inside loop -// int ThisForLoopAllTrue = 0; -// ASTVec ForloopVec; -// ForloopVec.push_back(ASTTrue); -// for(;paramCurrentValue < paramLimit;) -// { -// ASTNode currentFormula; -// ASTNode currentExceptFormula = exceptFormula; -// currentExceptFormula = -// SimplifyFormula(exceptFormula, false, ParamToCurrentValMap); -// if(ASTTrue == currentExceptFormula) -// { -// currentFormula = ASTTrue; -// } -// else -// { -// currentFormula = -// SimplifyFormula(formulabody, false, ParamToCurrentValMap); -// } - -// //Check the currentformula against the model, and add it to the -// //SAT solver if it is false against the model -// if(absrefine_flag && -// ASTTrue != currentFormula && -// ASTFalse == ComputeFormulaUsingModel(currentFormula)) -// { -// currentFormula = TransformFormula_TopLevel(currentFormula); -// res = -// CallSAT_ResultCheck(SatSolver, currentFormula, original_input); -// if(SOLVER_UNDECIDED != res) -// { -// return res; -// } -// } -// if(!absrefine_flag && -// ASTTrue != currentFormula) -// { -// currentFormula = TransformFormula_TopLevel(currentFormula); -// res = -// CallSAT_ResultCheck(SatSolver, currentFormula, original_input); -// if(SOLVER_UNDECIDED != res) -// { -// return res; -// } -// } - -// //Update ParamToCurrentValMap with parameter and its current -// //value. FIXME: Possible leak since I am not freeing the -// //previous 'value' for the same 'key' -// paramCurrentValue = paramCurrentValue + paramIncrement; -// (*ParamToCurrentValMap)[parameter] = -// CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue); -// } //end of expanding the FOR loop - -// return res; -// } //end of SATBased_FiniteLoop_Refinement - + } //end of Check_FiniteLoop_UsingModel };// end of namespace BEEV diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile index 33c6380..1d7a2d5 100644 --- a/tests/c-api-tests/Makefile +++ b/tests/c-api-tests/Makefile @@ -1,7 +1,7 @@ CXXFLAGS=-DEXT_HASH_MAP -m32 -I../../src/c_interface -L../../lib -all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 +all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 rm -rf *.out 0: @@ -61,7 +61,11 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 ./a17.out 18: g++ $(CXXFLAGS) cvc-to-c.cpp -lstp -o a18.out - ./a18.out ./t.cvc + #./a18.out ./t.cvc + +19: + g++ -g $(CXXFLAGS) biosat-rna.cpp -lstp -o biosat.out + time ./biosat.out AUUGGUAUGUAAGCUACUUCUUCCAGUAGCUGCGUCAUAACAUCAAGGUUAUGCAUACUGAGCCGAAGCUCAGCUUCGGUCCUCCAAGGAAGACCA 800 clean: diff --git a/tests/c-api-tests/biosat-rna.cpp b/tests/c-api-tests/biosat-rna.cpp index e246683..8ee559d 100644 --- a/tests/c-api-tests/biosat-rna.cpp +++ b/tests/c-api-tests/biosat-rna.cpp @@ -50,7 +50,7 @@ using namespace __gnu_cxx; struct eqint { bool operator()(int s1, int s2) const { - return (s1==s2); + return (s1 == s2); } }; @@ -134,8 +134,8 @@ int main(int argc, char** argv) { int idx2_bits_width = req_bits(seq_len*seq_len); int idx3_bits_width = req_bits(seq_len*seq_len*UNKNOWN_CONST*UNKNOWN_CONST); - hash_set, eqint> Ex_blacklist(100000); - hash_set, eqint> Ey_blacklist(100000); + hash_set, eqint> Ex_blacklist(10000); + hash_set, eqint> Ey_blacklist(10000); int E_table[36]; @@ -521,7 +521,7 @@ int main(int argc, char** argv) { int e_bitdiff = TOT_E_BITS - E_BITS; Expr padding = vc_bvConstExprFromInt(vc, e_bitdiff, 0); int count = 0; - Expr bvplus_terms[10000]; + Expr bvplus_terms[100000]; for(int i=0; i