Expr three = em.mkConst(new Rational(3));
Expr twox_plus_y_geq_3 = em.mkExpr(Kind.GEQ, twox_plus_y, three);
- BoolExpr formula =
- new BoolExpr(em.mkExpr(Kind.AND, x_positive, y_positive)).
- impExpr(new BoolExpr(twox_plus_y_geq_3));
+ Expr formula =
+ new Expr(em.mkExpr(Kind.AND, x_positive, y_positive)).
+ impExpr(new Expr(twox_plus_y_geq_3));
System.out.println("Checking validity of formula " + formula + " with CVC4.");
System.out.println("CVC4 should report VALID.");
let lhs = em->mkExpr(and_kind, x_positive, y_positive)
(* This fails for some reason. *)
-(* let rhs = new_BoolExpr(twox_plus_y_geq_3)
- let formula = new_BoolExpr(lhs)->impExpr(rhs) *)
+(* let rhs = new_Expr(twox_plus_y_geq_3)
+ let formula = new_Expr(lhs)->impExpr(rhs) *)
let formula = em->mkExpr(implies, lhs, twox_plus_y_geq_3)
-let bformula = new_BoolExpr(formula) in
+let bformula = new_Expr(formula) in
print_string "Checking validity of formula " ;
print_string (get_string (formula->toString ())) ;
my $three = $em->mkConst(new CVC4::Integer(3));
my $twox_plus_y_geq_3 = $em->mkExpr($CVC4::GEQ, $twox_plus_y, $three);
-my $formula = new CVC4::BoolExpr($em->mkExpr($CVC4::AND, $x_positive, $y_positive))->impExpr(new CVC4::BoolExpr($twox_plus_y_geq_3));
+my $formula = new CVC4::Expr($em->mkExpr($CVC4::AND, $x_positive, $y_positive))->impExpr(new CVC4::Expr($twox_plus_y_geq_3));
print "Checking validity of formula " . $formula->toString() . " with CVC4.\n";
print "CVC4 should report VALID.\n";
my $three = $em->mkConst(new CVC4::Integer(3));
my $twox_plus_y_geq_3 = $em->mkExpr($CVC4::GEQ, $twox_plus_y, $three);
-my $formula = new CVC4::BoolExpr($em->mkExpr($CVC4::AND, $x_positive, $y_positive))->impExpr(new CVC4::BoolExpr($twox_plus_y_geq_3));
+my $formula = new CVC4::Expr($em->mkExpr($CVC4::AND, $x_positive, $y_positive))->impExpr(new CVC4::Expr($twox_plus_y_geq_3));
print "Checking validity of formula " . $formula->toString() . " with CVC4.\n";
print "CVC4 should report VALID.\n";
####
import CVC4
-from CVC4 import ExprManager, SmtEngine, Integer, BoolExpr
+from CVC4 import ExprManager, SmtEngine, Integer, Expr
import sys
three = em.mkConst(Integer(3))
twox_plus_y_geq_3 = em.mkExpr(CVC4.GEQ, twox_plus_y, three)
- formula = BoolExpr(em.mkExpr(CVC4.AND, x_positive, y_positive)).impExpr(BoolExpr(twox_plus_y_geq_3))
+ formula = Expr(em.mkExpr(CVC4.AND, x_positive, y_positive)).impExpr(Expr(twox_plus_y_geq_3))
print "Checking validity of formula " + formula.toString() + " with CVC4."
print "CVC4 should report VALID."
three = em.mkConst(CVC4::Integer.new(3))
twox_plus_y_geq_3 = em.mkExpr(GEQ, twox_plus_y, three)
-formula = BoolExpr.new(em.mkExpr(AND, x_positive, y_positive)).impExpr(BoolExpr.new(twox_plus_y_geq_3))
+formula = Expr.new(em.mkExpr(AND, x_positive, y_positive)).impExpr(Expr.new(twox_plus_y_geq_3))
puts "Checking validity of formula " + formula.toString + " with CVC4."
puts "CVC4 should report VALID."
set three [ExprManager_mkConst em [Integer _ 3]]
set twox_plus_y_geq_3 [ExprManager_mkExpr em $GEQ $twox_plus_y $three]
-set formula [BoolExpr_impExpr [BoolExpr _1 [ExprManager_mkExpr em $AND $x_positive $y_positive]] [BoolExpr _2 $twox_plus_y_geq_3]]
+set formula [Expr_impExpr [Expr _1 [ExprManager_mkExpr em $AND $x_positive $y_positive]] [Expr _2 $twox_plus_y_geq_3]]
puts "Checking validity of formula [Expr_toString $formula] with CVC4."
puts "CVC4 should report VALID."
%include "util/array.i"
%include "util/array_store_all.i"
%include "util/hash.i"
+%include "util/util_model.i"
%include "expr/type.i"
%include "util/ascription_type.i"
if(! ok()) {
this->Command::printResult(out);
} else {
- d_smtEngine->printModel( out, d_result );
+ out << *d_result;
}
}
undocumented-alias --statistics = --stats
undocumented-alias --no-statistics = --no-stats
-common-option parseOnly parse-only --parse-only bool :read-write
+option parseOnly parse-only --parse-only bool :read-write
exit after parsing input
-common-option preprocessOnly preprocess-only --preprocess-only bool
+option preprocessOnly preprocess-only --preprocess-only bool
exit after preprocessing input
option segvNoSpin --segv-nospin bool
}
progress_char=/
+if [ -t 1 ]; then r="\r"; else r=""; fi
function progress {
file="$(expr "$1" : '.*\(.................................................................\)')"
if [ -z "$file" ]; then file="$1"; else file="[...]$file"; fi
- printf "\r%c %-70s (%3d%%)" "$progress_char" "$file" "$(($2*100/$3))"
+ [ -t 1 ] && printf "$r%c %-70s (%3d%%)" "$progress_char" "$file" "$(($2*100/$3))"
progress_char="`echo "$progress_char" | tr -- '-\\\\|/' '\\\\|/-'`"
}
function NOTE {
- printf "\r%-80s\n" "$kf:$lineno: note: $@"
+ printf "$r%-80s\n" "$kf:$lineno: note: $@"
}
function WARN {
- printf "\r%-80s\n" "$kf:$lineno: warning: $@"
+ printf "$r%-80s\n" "$kf:$lineno: warning: $@"
}
function ERR {
- printf "\r%-80s\n" "$kf:$lineno: error: $@"
+ printf "$r%-80s\n" "$kf:$lineno: error: $@"
exit 1
}
rm -f "$output.tmp"
else
mv -f "$output.tmp" "$output"
- printf "\rregenerated %-68s\n" "$output"
+ printf "${r}regenerated %-68s\n" "$output"
fi
}
regenerated=false
else
mv -f "$output.tmp" "$output"
- printf "\rregenerated %-68s\n" "$output"
+ printf "${r}regenerated %-68s\n" "$output"
regenerated=true
fi
rm -f "$output.tmp"
done
if ! $regenerated; then
- printf "\r%-80s\r" ""
+ [ -t 1 ] && printf "$r%-80s$r" ""
fi
Expr
Parser::mkFunction(const std::string& name, const Type& type,
- bool levelZero) {
+ bool levelZero) {
Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
Expr expr = d_exprManager->mkVar(name, type);
defineFunction(name, expr, levelZero);
| str[s]
{ sexpr = SExpr(s); }
| symbol[s,CHECK_NONE,SYM_SORT]
- { sexpr = SExpr(s); }
+ { sexpr = SExpr(SExpr::Keyword(s)); }
| builtinOp[k]
{ std::stringstream ss;
ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k);
}/* AstPrinter::toStream(CommandStatus*) */
-void AstPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() {
+void AstPrinter::toStream(std::ostream& out, Model& m) const throw() {
out << "Model()";
}
+void AstPrinter::toStream(std::ostream& out, Model& m, const Command* c) const throw() {
+ // shouldn't be called; only the non-Command* version above should be
+ Unreachable();
+}
+
static void toStream(std::ostream& out, const EmptyCommand* c) throw() {
out << "EmptyCommand(" << c->getName() << ")";
}
class AstPrinter : public CVC4::Printer {
void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
+ void toStream(std::ostream& out, Model& m, const Command* c) const throw();
public:
void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
void toStream(std::ostream& out, const CommandStatus* s) const throw();
- //for models
- void toStream(std::ostream& out, Model* m, const Command* c) const throw();
+ void toStream(std::ostream& out, Model& m) const throw();
};/* class AstPrinter */
}/* CVC4::printer::ast namespace */
}/* CvcPrinter::toStream(CommandStatus*) */
-void CvcPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() {
- theory::TheoryModel* tm = (theory::TheoryModel*)m;
+void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const throw() {
+ theory::TheoryModel& tm = (theory::TheoryModel&) m;
if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
if( tn.isSort() ){
//print the cardinality
- if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){
- out << "; cardinality of " << tn << " is " << tm->d_rep_set.d_type_reps[tn].size() << std::endl;
+ if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+ out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
}
}
out << c << std::endl;
if( tn.isSort() ){
//print the representatives
- if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){
- for( size_t i=0; i<tm->d_rep_set.d_type_reps[tn].size(); i++ ){
- if( tm->d_rep_set.d_type_reps[tn][i].isVar() ){
- out << tm->d_rep_set.d_type_reps[tn][i] << " : " << tn << ";" << std::endl;
+ if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+ for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
+ if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
+ out << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " : " << tn << ";" << std::endl;
}else{
- out << "% rep: " << tm->d_rep_set.d_type_reps[tn][i] << std::endl;
+ out << "% rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl;
}
}
}
}else{
out << tn;
}
- out << " = " << tm->getValue( n ) << ";" << std::endl;
+ out << " = " << tm.getValue( n ) << ";" << std::endl;
/*
//for table format (work in progress)
class CvcPrinter : public CVC4::Printer {
void toStream(std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const throw();
+ void toStream(std::ostream& out, Model& m, const Command* c) const throw();
public:
void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
void toStream(std::ostream& out, const CommandStatus* s) const throw();
- //for models
- void toStream(std::ostream& out, Model* m, const Command* c) const throw();
};/* class CvcPrinter */
}/* CVC4::printer::cvc namespace */
}
}/* Printer::toStream(SExpr) */
-void Printer::toStream(std::ostream& out, Model* m) const throw() {
- for(size_t i = 0; i < m->getNumCommands(); ++i) {
- toStream(out, m, m->getCommand(i));
+void Printer::toStream(std::ostream& out, Model& m) const throw() {
+ for(size_t i = 0; i < m.getNumCommands(); ++i) {
+ toStream(out, m, m.getCommand(i));
}
}/* Printer::toStream(Model) */
// derived classes can construct, but no one else.
Printer() throw() {}
+ /** write model response to command */
+ virtual void toStream(std::ostream& out, Model& m, const Command* c) const throw() = 0;
+
public:
/** Get the Printer for a given OutputLanguage */
static Printer* getPrinter(OutputLanguage lang) throw() {
virtual void toStream(std::ostream& out, const Result& r) const throw();
/** Write a Model out to a stream with this Printer. */
- virtual void toStream(std::ostream& out, Model* m ) const throw();
+ virtual void toStream(std::ostream& out, Model& m) const throw();
- //for models
-
- /** write model response to command */
- virtual void toStream(std::ostream& out, Model* m, const Command* c) const throw() = 0;
};/* class Printer */
}/* CVC4 namespace */
Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
}/* Smt1Printer::toStream() */
-void Smt1Printer::toStream(std::ostream& out, Model* m, const Command* c) const throw() {
- Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m, c);
+void Smt1Printer::toStream(std::ostream& out, Model& m) const throw() {
+ Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m);
+}
+
+void Smt1Printer::toStream(std::ostream& out, Model& m, const Command* c) const throw() {
+ // shouldn't be called; only the non-Command* version above should be
+ Unreachable();
}
}/* CVC4::printer::smt1 namespace */
namespace smt1 {
class Smt1Printer : public CVC4::Printer {
+ void toStream(std::ostream& out, Model& m, const Command* c) const throw();
public:
void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
void toStream(std::ostream& out, const CommandStatus* s) const throw();
void toStream(std::ostream& out, const SExpr& sexpr) const throw();
- //for models
- void toStream(std::ostream& out, Model* m, const Command* c) const throw();
+ void toStream(std::ostream& out, Model& m) const throw();
};/* class Smt1Printer */
}/* CVC4::printer::smt1 namespace */
}/* Smt2Printer::toStream(CommandStatus*) */
-void Smt2Printer::toStream(std::ostream& out, Model* m, const Command* c) const throw() {
- theory::TheoryModel* tm = (theory::TheoryModel*)m;
+void Smt2Printer::toStream(std::ostream& out, Model& m, const Command* c) const throw() {
+ theory::TheoryModel& tm = (theory::TheoryModel&) m;
if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
if( tn.isSort() ){
//print the cardinality
- if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){
- out << "; cardinality of " << tn << " is " << tm->d_rep_set.d_type_reps[tn].size() << std::endl;
+ if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+ out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
}
}
out << c << std::endl;
if( tn.isSort() ){
//print the representatives
- if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){
- for( size_t i=0; i<tm->d_rep_set.d_type_reps[tn].size(); i++ ){
- if( tm->d_rep_set.d_type_reps[tn][i].isVar() ){
- out << "(declare-fun " << tm->d_rep_set.d_type_reps[tn][i] << " () " << tn << ")" << std::endl;
+ if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+ for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
+ if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
+ out << "(declare-fun " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " () " << tn << ")" << std::endl;
}else{
- out << "; rep: " << tm->d_rep_set.d_type_reps[tn][i] << std::endl;
+ out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl;
}
}
}
}
} else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) {
Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() );
- Node val = tm->getValue( n );
+ Node val = tm.getValue( n );
if(val.getKind() == kind::LAMBDA) {
out << "(define-fun " << n << " " << val[0]
<< " " << n.getType().getRangeType()
class Smt2Printer : public CVC4::Printer {
void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
+ void toStream(std::ostream& out, Model& m, const Command* c) const throw();
public:
void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
void toStream(std::ostream& out, const CommandStatus* s) const throw();
- //for models
- void toStream(std::ostream& out, Model* m, const Command* c) const throw();
void toStream(std::ostream& out, const Result& r) const throw();
};/* class Smt2Printer */
trail_user_lim.push(trail.size());
assert(trail_user_lim.size() == assertionLevel);
- context->push();
+ context->push(); // SAT context for CVC4
Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel << ", trail.size is " << trail.size() << std::endl;
}
Debug("minisat") << "about to removeClausesAboveLevel(" << assertionLevel << ") in CNF" << std::endl;
- context->pop();
+ context->pop(); // SAT context for CVC4
// Notify the cnf
proxy->removeClausesAboveLevel(assertionLevel);
//Assert(d_inCheckSat, "Sat solver should be in solve()!");
Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
- if(!d_inCheckSat && Dump.isOn("learned")) {
- Dump("learned") << AssertCommand(node.toExpr());
- } else if(Dump.isOn("lemmas")) {
+ if(Dump.isOn("lemmas")) {
Dump("lemmas") << AssertCommand(node.toExpr());
}
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
declarations\n\
+ Dump user declarations. Implied by all following modes.\n\
\n\
-assertions\n\
-+ Output the assertions after non-clausal simplification and static\n\
- learning phases, but before presolve-time T-lemmas arrive. If\n\
- non-clausal simplification and static learning are off\n\
- (--simplification=none --no-static-learning), the output\n\
- will closely resemble the input (with term-level ITEs removed).\n\
-\n\
skolems\n\
+ Dump internally-created skolem variable declarations. These can\n\
arise from preprocessing simplifications, existential elimination,\n\
and a number of other things. Implied by all following modes.\n\
\n\
-learned\n\
-+ Output the assertions after non-clausal simplification, static\n\
- learning, and presolve-time T-lemmas. This should include all eager\n\
- T-lemmas (in the form provided by the theory, which my or may not be\n\
- clausal). Also includes level-0 BCP done by Minisat.\n\
+assertions\n\
++ Output the assertions after preprocessing and before clausification.\n\
+ Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
+ where PASS is one of the preprocessing passes: skolem-quant simplify\n\
+ static-learning ite-removal repeat-simplify theory-preprocessing.\n\
+ PASS can also be the special value \"everything\", in which case the\n\
+ assertions are printed before any preprocessing (with\n\
+ \"assertions:pre-everything\") or after all preprocessing completes\n\
+ (with \"assertions:post-everything\").\n\
\n\
clauses\n\
+ Do all the preprocessing outlined above, and dump the CNF-converted\n\
+ Output completeness queries for all full-check effort-level theory checks\n\
\n\
Dump modes can be combined with multiple uses of --dump. Generally you want\n\
-one from the assertions category (either assertions, learned, or clauses), and\n\
+one from the assertions category (either assertions or clauses), and\n\
perhaps one or more stateful or non-stateful modes for checking correctness\n\
and completeness of decision procedure implementations. Stateful modes dump\n\
the contextual assertions made by the core solver (all decisions and\n\
if(!strcmp(optargPtr, "benchmark")) {
} else if(!strcmp(optargPtr, "declarations")) {
} else if(!strcmp(optargPtr, "assertions")) {
+ Dump.on("assertions:post-everything");
+ } else if(!strncmp(optargPtr, "assertions:", 11)) {
+ const char* p = optargPtr + 11;
+ if(!strncmp(p, "pre-", 4)) {
+ p += 4;
+ } else if(!strncmp(p, "post-", 5)) {
+ p += 5;
+ } else {
+ throw OptionException(std::string("don't know how to dump `") +
+ optargPtr + "'. Please consult --dump help.");
+ }
+ if(!strcmp(p, "everything")) {
+ } else if(!strcmp(p, "skolem-quant")) {
+ } else if(!strcmp(p, "simplify")) {
+ } else if(!strcmp(p, "static-learning")) {
+ } else if(!strcmp(p, "ite-removal")) {
+ } else if(!strcmp(p, "repeat-simplify")) {
+ } else if(!strcmp(p, "theory-preprocessing")) {
+ } else {
+ throw OptionException(std::string("don't know how to dump `") +
+ optargPtr + "'. Please consult --dump help.");
+ }
+ Dump.on("assertions");
} else if(!strcmp(optargPtr, "skolems")) {
- } else if(!strcmp(optargPtr, "learned")) {
} else if(!strcmp(optargPtr, "clauses")) {
} else if(!strcmp(optargPtr, "t-conflicts") ||
!strcmp(optargPtr, "t-lemmas") ||
Dump.on("benchmark");
if(strcmp(optargPtr, "benchmark")) {
Dump.on("declarations");
- if(strcmp(optargPtr, "declarations") && strcmp(optargPtr, "assertions")) {
+ if(strcmp(optargPtr, "declarations")) {
Dump.on("skolems");
}
}
** Major contributors: dejan
** Minor contributors (to current version): cconway, kshitij
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
/** Assertions to push to sat */
vector<Node> d_assertionsToCheck;
- /** Map from skolem variables to index in d_assertionsToCheck containing
- * corresponding introduced Boolean ite */
+ /**
+ * Map from skolem variables to index in d_assertionsToCheck containing
+ * corresponding introduced Boolean ite
+ */
IteSkolemMap d_iteSkolemMap;
+public:
+ /** Instance of the ITE remover */
+ RemoveITE d_iteRemover;
+
+private:
/** The top level substitutions */
SubstitutionMap d_topLevelSubstitutions;
*/
bool simplifyAssertions() throw(TypeCheckingException);
- /**
- * contains quantifiers
- */
- bool containsQuantifiers( Node n );
-
public:
SmtEnginePrivate(SmtEngine& smt) :
d_smt(smt),
+ d_assertionsToPreprocess(),
d_nonClausalLearnedLiterals(),
+ d_realAssertionsEnd(0),
d_propagator(d_nonClausalLearnedLiterals, true, true),
+ d_assertionsToCheck(),
+ d_iteSkolemMap(),
+ d_iteRemover(smt.d_userContext),
d_topLevelSubstitutions(smt.d_userContext),
d_lastSubstitutionPos(smt.d_userContext, d_topLevelSubstitutions.end()) {
d_smt.d_nodeManager->subscribeEvents(this);
d_assertionsToPreprocess.clear();
d_nonClausalLearnedLiterals.clear();
d_assertionsToCheck.clear();
+ d_realAssertionsEnd = 0;
+ d_iteSkolemMap.clear();
}
/**
// We have mutual dependency here, so we add the prop engine to the theory
// engine later (it is non-essential there)
- d_theoryEngine = new TheoryEngine(d_context, d_userContext, const_cast<const LogicInfo&>(d_logic));
+ d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic));
// Add the theories
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
// Set the options for the theoryOf
if(!options::theoryOfMode.wasSetByUser()) {
if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) {
- Theory::setTheoryOfMode(theory::THEORY_OF_TERM_BASED);
+ Theory::setTheoryOfMode(THEORY_OF_TERM_BASED);
} else {
- Theory::setTheoryOfMode(theory::THEORY_OF_TYPE_BASED);
+ Theory::setTheoryOfMode(THEORY_OF_TYPE_BASED);
}
} else {
Theory::setTheoryOfMode(options::theoryOfMode());
d_logic = value.getValue();
setLogicInternal();
return;
+ } else {
+ throw UnrecognizedOptionException();
}
}
}
key == "source" ||
key == "category" ||
key == "difficulty" ||
- key == "smt-lib-version" ||
key == "notes") {
// ignore these
return;
+ } else if(key == "smt-lib-version") {
+ if( (value.isInteger() && value.getIntegerValue() == Integer(2)) ||
+ (value.isRational() && value.getRationalValue() == Rational(2)) ||
+ (value.getValue() == "2") ) {
+ // supported SMT-LIB version
+ return;
+ }
+ Warning() << "Warning: unsupported smt-lib-version: " << value << endl;
+ throw UnrecognizedOptionException();
} else if(key == "status") {
string s;
if(value.isAtom()) {
}
}
+// check if the given node contains a universal quantifier
+static bool containsQuantifiers(Node n) {
+ if(n.getKind() == kind::FORALL) {
+ return true;
+ } else {
+ for(unsigned i = 0; i < n.getNumChildren(); ++i) {
+ if(containsQuantifiers(n[i])) {
+ return true;
+ }
+ }
+ return false;
+ }
+}
+
Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< Node >& fvs ){
Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << std::endl;
if( n.getKind()==kind::NOT ){
Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl;
// Remove all of the ITE occurrences and normalize
- RemoveITE::run(d_assertionsToCheck, d_iteSkolemMap);
+ d_iteRemover.run(d_assertionsToCheck, d_iteSkolemMap);
for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
d_assertionsToCheck[i] = Rewriter::rewrite(d_assertionsToCheck[i]);
}
}
}
+// do dumping (before/after any preprocessing pass)
+static void dumpAssertions(const char* key,
+ const std::vector<Node>& assertionList) {
+ if( Dump.isOn("assertions") &&
+ Dump.isOn(std::string("assertions:") + key) ) {
+ // Push the simplified assertions to the dump output stream
+ for(unsigned i = 0; i < assertionList.size(); ++ i) {
+ TNode n = assertionList[i];
+ Dump("assertions") << AssertCommand(Expr(n.toExpr()));
+ }
+ }
+}
// returns false if it learns a conflict
bool SmtEnginePrivate::nonClausalSimplify() {
NodeBuilder<> learnedBuilder(kind::AND);
Assert(d_realAssertionsEnd <= d_assertionsToCheck.size());
- learnedBuilder << d_assertionsToCheck[d_realAssertionsEnd-1];
+ learnedBuilder << d_assertionsToCheck[d_realAssertionsEnd - 1];
if( options::incrementalSolving() ||
options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL ) {
}
if(learnedBuilder.getNumChildren() > 1) {
- d_assertionsToCheck[d_realAssertionsEnd-1] = Rewriter::rewrite(Node(learnedBuilder));
+ d_assertionsToCheck[d_realAssertionsEnd - 1] =
+ Rewriter::rewrite(Node(learnedBuilder));
}
d_propagator.finish();
Trace("simplify") << "SmtEnginePrivate::simplify(): "
<< " doing repeated simplification" << std::endl;
d_assertionsToCheck.swap(d_assertionsToPreprocess);
+ Assert(d_assertionsToCheck.empty());
bool noConflict = nonClausalSimplify();
- if(!noConflict) return false;
+ if(!noConflict) {
+ return false;
+ }
}
Trace("smt") << "POST repeatSimp" << std::endl;
return true;
}
-
-bool SmtEnginePrivate::containsQuantifiers( Node n ){
- if( n.getKind()==kind::FORALL ){
- return true;
- }else{
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( containsQuantifiers( n[i] ) ){
- return true;
- }
- }
- return false;
- }
-}
-
Result SmtEngine::check() {
Assert(d_fullyInited);
Assert(d_pendingPops == 0);
Assert(d_smt.d_fullyInited);
Assert(d_smt.d_pendingPops == 0);
+ // Dump the assertions
+ dumpAssertions("pre-everything", d_assertionsToPreprocess);
+
Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
- // any assertions added beyond realAssertionsEnd must NOT affect the equisatisfiability
+ Assert(d_assertionsToCheck.size() == 0);
+
+ // any assertions added beyond realAssertionsEnd must NOT affect the
+ // equisatisfiability
d_realAssertionsEnd = d_assertionsToPreprocess.size();
- if (d_realAssertionsEnd == 0) {
+ if(d_realAssertionsEnd == 0) {
+ // nothing to do
return;
}
Trace("simplify") << " got " << d_assertionsToPreprocess[i] << endl;
}
+ dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);
if( options::preSkolemQuant() ){
//apply pre-skolemization to existential quantifiers
for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
}
}
}
+ dumpAssertions("post-skolem-quant", d_assertionsToPreprocess);
+ dumpAssertions("pre-simplify", d_assertionsToPreprocess);
Chat() << "simplifying assertions..." << endl;
bool noConflict = simplifyAssertions();
+ dumpAssertions("post-simplify", d_assertionsToPreprocess);
+ dumpAssertions("pre-static-learning", d_assertionsToCheck);
if(options::doStaticLearning()) {
// Perform static learning
Chat() << "doing static learning..." << endl;
<< "performing static learning" << endl;
staticLearning();
}
+ dumpAssertions("post-static-learning", d_assertionsToCheck);
+ dumpAssertions("pre-ite-removal", d_assertionsToCheck);
{
Chat() << "removing term ITEs..." << endl;
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_iteRemovalTime);
removeITEs();
d_smt.d_stats->d_numAssertionsPost += d_assertionsToCheck.size();
}
+ dumpAssertions("post-ite-removal", d_assertionsToCheck);
+ dumpAssertions("pre-repeat-simplify", d_assertionsToCheck);
if(options::repeatSimp()) {
d_assertionsToCheck.swap(d_assertionsToPreprocess);
Chat() << "simplifying assertions..." << endl;
IteSkolemMap::iterator it = d_iteSkolemMap.begin();
IteSkolemMap::iterator iend = d_iteSkolemMap.end();
NodeBuilder<> builder(kind::AND);
- builder << d_assertionsToCheck[d_realAssertionsEnd-1];
+ builder << d_assertionsToCheck[d_realAssertionsEnd - 1];
for (; it != iend; ++it) {
if (d_topLevelSubstitutions.hasSubstitution((*it).first)) {
builder << d_assertionsToCheck[(*it).second];
}
}
if(builder.getNumChildren() > 1) {
- d_assertionsToCheck[d_realAssertionsEnd-1] = Rewriter::rewrite(Node(builder));
+ d_assertionsToCheck[d_realAssertionsEnd - 1] =
+ Rewriter::rewrite(Node(builder));
}
// For some reason this is needed for some benchmarks, such as
// http://church.cims.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
// Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size());
}
}
+ dumpAssertions("post-repeat-simplify", d_assertionsToCheck);
// begin: INVARIANT to maintain: no reordering of assertions or
// introducing new ones
Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ dumpAssertions("pre-theory-preprocessing", d_assertionsToCheck);
{
Chat() << "theory preprocessing..." << endl;
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime);
d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]);
}
}
-
- if(Dump.isOn("assertions")) {
- // Push the simplified assertions to the dump output stream
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
- Dump("assertions")
- << AssertCommand(d_assertionsToCheck[i].toExpr());
- }
- }
+ dumpAssertions("post-theory-preprocessing", d_assertionsToCheck);
// Push the formula to decision engine
if(noConflict) {
// end: INVARIANT to maintain: no reordering of assertions or
// introducing new ones
+ dumpAssertions("post-everything", d_assertionsToCheck);
+
// Push the formula to SAT
{
Chat() << "converting to CNF..." << endl;
}
}
-Result SmtEngine::checkSat(const Expr& e) throw(TypeCheckingException) {
+Result SmtEngine::checkSat(const Expr& e) throw(TypeCheckingException, ModalException) {
Assert(e.isNull() || e.getExprManager() == d_exprManager);
return r;
}/* SmtEngine::checkSat() */
-Result SmtEngine::query(const Expr& e) throw(TypeCheckingException) {
+Result SmtEngine::query(const Expr& e) throw(TypeCheckingException, ModalException) {
Assert(!e.isNull());
Assert(e.getExprManager() == d_exprManager);
return d_private->expandDefinitions(Node::fromExpr(e), cache).toExpr();
}
-Expr SmtEngine::getValue(const Expr& e)
- throw(ModalException) {
+Expr SmtEngine::getValue(const Expr& e) throw(ModalException) {
Assert(e.getExprManager() == d_exprManager);
SmtScope smts(this);
throw ModalException(msg);
}
- // do not need to apply preprocessing substitutions (should be recorded in model already)
+ // do not need to apply preprocessing substitutions (should be recorded
+ // in model already)
- // Normalize for the theories
- Node n = Rewriter::rewrite( e.getNode() );
+ // Expand, then normalize
+ Node n = expandDefinitions(e).getNode();
+ n = Rewriter::rewrite(n);
Trace("smt") << "--- getting value of " << n << endl;
- theory::TheoryModel* m = d_theoryEngine->getModel();
+ TheoryModel* m = d_theoryEngine->getModel();
Node resultNode;
if( m ){
resultNode = m->getValue( n );
Node n = Rewriter::rewrite(*i);
Trace("smt") << "--- getting value of " << n << endl;
- theory::TheoryModel* m = d_theoryEngine->getModel();
+ TheoryModel* m = d_theoryEngine->getModel();
Node resultNode;
if( m ){
resultNode = m->getValue( n );
// and if Notice() is on, the user gave --verbose (or equivalent).
Notice() << "SmtEngine::checkModel(): generating model" << endl;
- theory::TheoryModel* m = d_theoryEngine->getModel();
+ TheoryModel* m = d_theoryEngine->getModel();
if(Notice.isOn()) {
- printModel(Notice.getStream(), m);
+ // This operator<< routine is non-const (i.e., takes a non-const Model&).
+ // This confuses the Notice() output routines, so extract the ostream
+ // from it and output it "manually." Should be fixed by making Model
+ // accessors const.
+ Notice.getStream() << *m;
}
// We have a "fake context" for the substitution map (we don't need it
// to be context-dependent)
context::Context fakeContext;
- theory::SubstitutionMap substitutions(&fakeContext);
+ SubstitutionMap substitutions(&fakeContext);
for(size_t k = 0; k < m->getNumCommands(); ++k) {
const DeclareFunctionCommand* c = dynamic_cast<const DeclareFunctionCommand*>(m->getCommand(k));
// now check if n contains func by doing a substitution
// [func->func2] and checking equality of the Nodes.
// (this just a way to check if func is in n.)
- theory::SubstitutionMap subs(&fakeContext);
+ SubstitutionMap subs(&fakeContext);
Node func2 = NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func.getType()), "", NodeManager::SKOLEM_NO_NOTIFY);
subs.addSubstitution(func, func2);
if(subs.apply(n) != n) {
n = Node::fromExpr(simplify(n.toExpr()));
Notice() << "SmtEngine::checkModel(): -- simplifies to " << n << endl;
+ TheoryId thy = Theory::theoryOf(n);
+ if(thy == THEORY_QUANTIFIERS || thy == THEORY_REWRITERULES) {
+ // Note this "skip" is done here, rather than above. This is
+ // because (1) the quantifier could in principle simplify to false,
+ // which should be reported, and (2) checking for the quantifier
+ // above, before simplification, doesn't catch buried quantifiers
+ // anyway (those not at the top-level).
+ Notice() << "SmtEngine::checkModel(): -- skipping quantified assertion"
+ << endl;
+ continue;
+ }
+
// The result should be == true.
if(n != NodeManager::currentNM()->mkConst(true)) {
- Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***" << endl;
+ Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
+ << endl;
stringstream ss;
ss << "SmtEngine::checkModel(): "
<< "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
#endif /* CVC4_PROOF */
}
-vector<Expr> SmtEngine::getAssertions()
- throw(ModalException) {
+vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
SmtScope smts(this);
finalOptionsAreSet();
if(Dump.isOn("benchmark")) {
return vector<Expr>(d_assertionList->begin(), d_assertionList->end());
}
-void SmtEngine::push() {
+void SmtEngine::push() throw(ModalException) {
SmtScope smts(this);
finalOptionsAreSet();
doPendingPops();
<< d_userContext->getLevel() << endl;
}
-void SmtEngine::pop() {
+void SmtEngine::pop() throw(ModalException) {
SmtScope smts(this);
finalOptionsAreSet();
Trace("smt") << "SMT pop()" << endl;
if(options::incrementalSolving()) {
d_private->processAssertions();
d_userContext->push();
- d_context->push();
+ // the d_context push is done inside of the SAT solver
d_propEngine->push();
}
}
Assert(d_pendingPops == 0 || options::incrementalSolving());
while(d_pendingPops > 0) {
d_propEngine->pop();
- d_context->pop();
+ // the d_context pop is done inside of the SAT solver
d_userContext->pop();
--d_pendingPops;
}
return d_statisticsRegistry->getStatistic(name);
}
-void SmtEngine::printModel( std::ostream& out, Model* m ){
- SmtScope smts(this);
- Expr::dag::Scope scope(out, false);
- Printer::getPrinter(options::outputLanguage())->toStream( out, m );
-}
-
-void SmtEngine::setUserAttribute( std::string& attr, Expr expr ){
+void SmtEngine::setUserAttribute(std::string& attr, Expr expr) {
SmtScope smts(this);
- d_theoryEngine->setUserAttribute( attr, expr.getNode() );
+ d_theoryEngine->setUserAttribute(attr, expr.getNode());
}
}/* CVC4 namespace */
smt::SmtEngineStatistics* d_stats;
/**
- * Add to Model command. This is used for recording a command that should be reported
- * during a get-model call.
+ * Add to Model command. This is used for recording a command
+ * that should be reported during a get-model call.
*/
void addToModelCommand(Command* c);
* of assertions by asserting the query expression's negation and
* calling check(). Returns valid, invalid, or unknown result.
*/
- Result query(const Expr& e) throw(TypeCheckingException);
+ Result query(const Expr& e) throw(TypeCheckingException, ModalException);
/**
* Assert a formula (if provided) to the current context and call
* check(). Returns sat, unsat, or unknown result.
*/
- Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException);
+ Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException, ModalException);
/**
* Simplify a formula without doing "much" work. Does not involve
/**
* Push a user-level context.
*/
- void push();
+ void push() throw(ModalException);
/**
* Pop a user-level context. Throws an exception if nothing to pop.
*/
- void pop();
+ void pop() throw(ModalException);
/**
* Interrupt a running query. This can be called from another thread
}
/**
- * print model function (need this?)
+ * Set user attribute.
+ * This function is called when an attribute is set by a user.
+ * In SMT-LIBv2 this is done via the syntax (! expr :attr)
*/
- void printModel( std::ostream& out, Model* m );
-
- /** Set user attribute
- * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done
- * via the syntax (! expr :attr)
- */
void setUserAttribute( std::string& attr, Expr expr );
};/* class SmtEngine */
d_index(type.getArrayIndexType()),
d_constituentType(type.getArrayConstituentType()),
d_nm(NodeManager::currentNM()),
- d_finished(false)
+ d_indexVec(),
+ d_constituentVec(),
+ d_finished(false),
+ d_arrayConst()
{
d_indexVec.push_back(*d_index);
d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
d_arrayConst = d_nm->mkConst(ArrayStoreAll(type.toType(), (*(*d_constituentVec.back())).toExpr()));
}
+ // An array enumerator could be large, and generally you don't want to
+ // go around copying these things; but a copy ctor is presently required
+ // by the TypeEnumerator framework.
+ ArrayEnumerator(const ArrayEnumerator& ae) throw() :
+ TypeEnumeratorBase<ArrayEnumerator>(ae.d_nm->mkArrayType(ae.d_index.getType(), ae.d_constituentType)),
+ d_index(ae.d_index),
+ d_constituentType(ae.d_constituentType),
+ d_nm(ae.d_nm),
+ d_indexVec(ae.d_indexVec),
+ d_constituentVec(),// copied below
+ d_finished(ae.d_finished),
+ d_arrayConst(ae.d_arrayConst)
+ {
+ for(std::vector<TypeEnumerator*>::const_iterator i =
+ ae.d_constituentVec.begin(), i_end = ae.d_constituentVec.end();
+ i != i_end;
+ ++i) {
+ d_constituentVec.push_back(new TypeEnumerator(**i));
+ }
+ }
+
~ArrayEnumerator() {
while (!d_constituentVec.empty()) {
delete d_constituentVec.back();
}
}
-void TheoryModel::toStream( std::ostream& out )
-{
- out << this;
-}
-
Node TheoryModel::getModelValue( TNode n )
{
if( n.isConst() ) {
}
} while (changed);
+#ifdef CVC4_ASSERTIONS
if (fullModel) {
// Assert that all representatives have been converted to constants
for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) {
Assert(repSet.empty());
}
}
+#endif /* CVC4_ASSERTIONS */
Trace("model-builder") << "Copy representatives to model..." << std::endl;
tm->d_reps.clear();
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
Expr getValue( Expr expr );
/** get cardinality for sort */
Cardinality getCardinality( Type t );
- /** to stream function */
- void toStream( std::ostream& out );
public:
/** print representative debug function */
void printRepresentativeDebug( const char* c, Node r );
typedef std::hash_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap;
typedef std::hash_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap;
typedef TypeSetMap::iterator iterator;
+ typedef TypeSetMap::const_iterator const_iterator;
private:
TypeSetMap d_typeSet;
TypeToTypeEnumMap d_teMap;
s->insert(n);
}
- std::set<Node>* getSet(TypeNode t)
+ std::set<Node>* getSet(TypeNode t) const
{
- iterator it = d_typeSet.find(t);
+ const_iterator it = d_typeSet.find(t);
if (it == d_typeSet.end()) {
return NULL;
}
return TheoryModel::getInterpretedValue( n );
}
-void FirstOrderModel::toStream(std::ostream& out){
-
-}
-
//for evaluation of quantifier bodies
public:
// initialize the model
void initialize( bool considerAxioms = true );
- /** to stream function */
- void toStream( std::ostream& out );
//the following functions are for evaluating quantifier bodies
public:
/** reset evaluation */
TheoryEngine::TheoryEngine(context::Context* context,
context::UserContext* userContext,
+ RemoveITE& iteRemover,
const LogicInfo& logicInfo)
: d_propEngine(NULL),
d_decisionEngine(NULL),
d_propagationMapTimestamp(context, 0),
d_propagatedLiterals(context),
d_propagatedLiteralsIndex(context, 0),
+ d_iteRemover(iteRemover),
d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
+ d_true(),
+ d_false(),
d_interrupted(false),
d_inPreregister(false),
d_factsAsserted(context, false),
std::vector<Node> additionalLemmas;
IteSkolemMap iteSkolemMap;
additionalLemmas.push_back(node);
- RemoveITE::run(additionalLemmas, iteSkolemMap);
+ d_iteRemover.run(additionalLemmas, iteSkolemMap);
additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]);
// assert to prop engine
*/
theory::LemmaStatus lemma(TNode node, bool negated, bool removable);
+ RemoveITE& d_iteRemover;
+
/** Time spent in theory combination */
TimerStat d_combineTheoriesTime;
public:
/** Constructs a theory engine */
- TheoryEngine(context::Context* context, context::UserContext* userContext, const LogicInfo& logic);
+ TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveITE& iteRemover, const LogicInfo& logic);
/** Destroys a theory engine */
~TheoryEngine();
array_store_all.i \
ascription_type.i \
rational.i \
- hash.i
+ hash.i \
+ util_model.i
DISTCLEANFILES = \
integer.h.tmp \
namespace CVC4 {
-struct IteRewriteAttrTag {};
-typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr;
-
void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
{
for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
Debug("ite") << "removeITEs(" << node << ")" << endl;
// The result may be cached already
- Node cachedRewrite;
NodeManager *nodeManager = NodeManager::currentNM();
- if(nodeManager->getAttribute(node, IteRewriteAttr(), cachedRewrite)) {
+ ITECache::iterator i = d_iteCache.find(node);
+ if(i != d_iteCache.end()) {
+ Node cachedRewrite = (*i).second;
Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl;
return cachedRewrite.isNull() ? Node(node) : cachedRewrite;
}
Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
// Attach the skolem
- nodeManager->setAttribute(node, IteRewriteAttr(), skolem);
+ d_iteCache[node] = skolem;
// Remove ITEs from the new assertion, rewrite it and push it to the output
newAssertion = run(newAssertion, output, iteSkolemMap);
// If changes, we rewrite
if(somethingChanged) {
- cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
- nodeManager->setAttribute(node, IteRewriteAttr(), cachedRewrite);
+ Node cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
+ d_iteCache[node] = cachedRewrite;
return cachedRewrite;
} else {
- nodeManager->setAttribute(node, IteRewriteAttr(), Node::null());
+ d_iteCache[node] = Node::null();
return node;
}
} else {
- nodeManager->setAttribute(node, IteRewriteAttr(), Node::null());
+ d_iteCache[node] = Node::null();
return node;
}
}
#include <vector>
#include "expr/node.h"
#include "util/dump.h"
+#include "context/context.h"
+#include "context/cdhashmap.h"
namespace CVC4 {
typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
class RemoveITE {
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> ITECache;
+ ITECache d_iteCache;
public:
+ RemoveITE(context::UserContext* u) :
+ d_iteCache(u) {
+ }
+
/**
* Removes the ITE nodes by introducing skolem variables. All
* additional assertions are pushed into assertions. iteSkolemMap
* assertions containing the new Boolean ite created in conjunction
* with that skolem variable.
*/
- static void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap);
+ void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap);
/**
* Removes the ITE from the node by introducing skolem
* variables to the index in assertions containing the new Boolean
* ite created in conjunction with that skolem variable.
*/
- static Node run(TNode node, std::vector<Node>& additionalAssertions,
- IteSkolemMap& iteSkolemMap);
+ Node run(TNode node, std::vector<Node>& additionalAssertions,
+ IteSkolemMap& iteSkolemMap);
};/* class RemoveTTE */
#include "expr/command.h"
#include "smt/smt_engine_scope.h"
#include "smt/command_list.h"
+#include "printer/printer.h"
#include <vector>
namespace CVC4 {
+std::ostream& operator<<(std::ostream& out, Model& m) {
+ smt::SmtScope smts(&m.d_smt);
+ Expr::dag::Scope scope(out, false);
+ Printer::getPrinter(options::outputLanguage())->toStream(out, m);
+ return out;
+}
+
Model::Model() :
d_smt(*smt::currentSmtEngine()) {
}
class CVC4_PUBLIC Command;
class CVC4_PUBLIC SmtEngine;
+class CVC4_PUBLIC Model;
+
+std::ostream& operator<<(std::ostream&, Model&) CVC4_PUBLIC;
class CVC4_PUBLIC Model {
-private:
+ friend std::ostream& operator<<(std::ostream&, Model&);
+
+protected:
/** The SmtEngine we're associated to */
const SmtEngine& d_smt;
-public:
- /** construct the base class */
+
+ /** construct the base class; users cannot do this, only CVC4 internals */
Model();
+
+public:
/** virtual destructor */
virtual ~Model() { }
/** get number of commands to report */
virtual Expr getValue(Expr expr) = 0;
/** get cardinality for sort */
virtual Cardinality getCardinality(Type t) = 0;
- /** write the model to a stream */
- virtual void toStream(std::ostream& out) = 0;
};/* class Model */
class ModelBuilder
--- /dev/null
+%{
+#include "util/util_model.h"
+%}
+
+%include "util/util_model.h"
BUG_TESTS = \
bug216.smt2 \
bug233.cvc \
- bug326.smt2
+ bug326.smt2 \
+ bug394.smt2 \
+ bug396.smt2
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
EXTRA_DIST = $(TESTS) \
- bug216.smt2.expect \
- bug394.smt2 \
- bug396.smt2
+ bug216.smt2.expect
# synonyms for "check" in this directory
.PHONY: regress regress0 test
;(set-option :produce-unsat-cores true)\r
(set-option :print-success false)\r
(set-info :smt-lib-version 2.0)\r
-(set-option :produce-models true)\r
+;(set-option :produce-models true)\r
(set-logic ALL_SUPPORTED)\r
; done setting options\r
\r
_b45) $getIdx)\r
))\r
(check-sat)\r
-(get-value ((ControlFlow 0 0)))\r
-(get-value ((ControlFlow 0 9318)))\r
-(get-value ((ControlFlow 0 823)))\r
+;(get-value ((ControlFlow 0 0)))\r
+;(get-value ((ControlFlow 0 9318)))\r
+;(get-value ((ControlFlow 0 823)))\r
(assert (not (= (ControlFlow 0 823) (- 10729))))\r
(check-sat)\r
(pop 1)\r
_b45) $DCT)\r
))\r
(check-sat)\r
-(get-value ((ControlFlow 0 0)))\r
-(get-value ((ControlFlow 0 11167)))\r
-(get-value ((ControlFlow 0 4117)))\r
-(get-value ((ControlFlow 0 4199)))\r
+;(get-value ((ControlFlow 0 0)))\r
+;(get-value ((ControlFlow 0 11167)))\r
+;(get-value ((ControlFlow 0 4117)))\r
+;(get-value ((ControlFlow 0 4199)))\r
(assert (not (= (ControlFlow 0 4199) (- 13495))))\r
(check-sat)\r
-(get-value ((ControlFlow 0 0)))\r
-(get-value ((ControlFlow 0 11167)))\r
-(get-value ((ControlFlow 0 4117)))\r
-(get-value ((ControlFlow 0 4199)))\r
+;(get-value ((ControlFlow 0 0)))\r
+;(get-value ((ControlFlow 0 11167)))\r
+;(get-value ((ControlFlow 0 4117)))\r
+;(get-value ((ControlFlow 0 4199)))\r
(assert (not (= (ControlFlow 0 4199) (- 13487))))\r
(check-sat)\r
-(get-value ((ControlFlow 0 0)))\r
-(get-value ((ControlFlow 0 11167)))\r
-(get-value ((ControlFlow 0 4117)))\r
-(get-value ((ControlFlow 0 4199)))\r
+;(get-value ((ControlFlow 0 0)))\r
+;(get-value ((ControlFlow 0 11167)))\r
+;(get-value ((ControlFlow 0 4117)))\r
+;(get-value ((ControlFlow 0 4199)))\r
(assert (not (= (ControlFlow 0 4199) (- 13509))))\r
(check-sat)\r
-(get-value ((ControlFlow 0 0)))\r
-(get-value ((ControlFlow 0 11167)))\r
-(get-value ((ControlFlow 0 4117)))\r
-(get-value ((ControlFlow 0 4199)))\r
+;(get-value ((ControlFlow 0 0)))\r
+;(get-value ((ControlFlow 0 11167)))\r
+;(get-value ((ControlFlow 0 4117)))\r
+;(get-value ((ControlFlow 0 4199)))\r
(assert (not (= (ControlFlow 0 4199) (- 13553))))\r
(check-sat)\r
-(get-value ((ControlFlow 0 0)))\r
-(get-value ((ControlFlow 0 11167)))\r
-(get-value ((ControlFlow 0 4117)))\r
-(get-value ((ControlFlow 0 4199)))\r
+;(get-value ((ControlFlow 0 0)))\r
+;(get-value ((ControlFlow 0 11167)))\r
+;(get-value ((ControlFlow 0 4117)))\r
+;(get-value ((ControlFlow 0 4199)))\r
(pop 1)\r
(push 1)\r
(set-info :boogie-vc-id $DCT)\r
_b45) $DCT)\r
))\r
(check-sat)\r
-(get-value ((ControlFlow 0 0)))\r
-(get-value ((ControlFlow 0 11167)))\r
-(get-value ((ControlFlow 0 4117)))\r
-(get-value ((ControlFlow 0 4199)))\r
+;(get-value ((ControlFlow 0 0)))\r
+;(get-value ((ControlFlow 0 11167)))\r
+;(get-value ((ControlFlow 0 4117)))\r
+;(get-value ((ControlFlow 0 4199)))\r
(assert (not (= (ControlFlow 0 4199) (- 13575))))\r
(check-sat)\r
-(get-value ((ControlFlow 0 0)))\r
-(get-value ((ControlFlow 0 11167)))\r
-(get-value ((ControlFlow 0 4117)))\r
-(get-value ((ControlFlow 0 4199)))\r
+;(get-value ((ControlFlow 0 0)))\r
+;(get-value ((ControlFlow 0 11167)))\r
+;(get-value ((ControlFlow 0 4117)))\r
+;(get-value ((ControlFlow 0 4199)))\r
(assert (not (= (ControlFlow 0 4199) (- 13712))))\r
(check-sat)\r
-(get-value ((ControlFlow 0 0)))\r
-(get-value ((ControlFlow 0 11167)))\r
-(get-value ((ControlFlow 0 4117)))\r
-(get-value ((ControlFlow 0 4199)))\r
+;(get-value ((ControlFlow 0 0)))\r
+;(get-value ((ControlFlow 0 11167)))\r
+;(get-value ((ControlFlow 0 4117)))\r
+;(get-value ((ControlFlow 0 4199)))\r
(assert (not (= (ControlFlow 0 4199) (- 13700))))\r
(check-sat)\r
FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 \
stalmark_e7_27_e7_31.ec.minimized.smt2 \
stalmark_e7_27_e7_31.ec.smt2 \
- tiny.smt2
+ tiny.smt2 \
+ speed2_e8_449_e8_517.ec.smt2 \
+ microwave21.ec.minimized.smt2
# simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2
# javafe.ast.StandardPrettyPrint.319_no_forall.smt2
# javafe.ast.WhileStmt.447_no_forall.smt2
-# CURRENTLY FAILING:
-# speed2_e8_449_e8_517.ec.smt2
-# microwave21.ec.minimized.smt2
-
# Regression tests for PL inputs
CVC_TESTS =
; initialize_defs
; PROPERTY DEFGEN
(set-logic QF_UFNIA)
-(set-info :status sat)
+(set-info :status unsat)
(declare-fun _base () Int)
(declare-fun _n () Int)
(assert (>= _n 0))
; not refinement_pass
(assert (not (=> (= _base (- 0 1)) (and (P (- 0 1)) (P 0)))))
(assert true)
-(check-sat)
\ No newline at end of file
+(check-sat)
import edu.nyu.acsys.CVC4.ExprManager;
import edu.nyu.acsys.CVC4.Expr;
import edu.nyu.acsys.CVC4.Type;
-import edu.nyu.acsys.CVC4.BoolExpr;
import edu.nyu.acsys.CVC4.Kind;
import edu.nyu.acsys.CVC4.Result;
import edu.nyu.acsys.CVC4.Configuration;
Type t = em.booleanType();
Expr a = em.mkVar("a", em.booleanType());
Expr b = em.mkVar("b", em.booleanType());
- BoolExpr e = new BoolExpr(em.mkExpr(Kind.AND, a, b, new BoolExpr(a).notExpr()));
+ Expr e = new Expr(em.mkExpr(Kind.AND, a, b, new Expr(a).notExpr()));
System.out.println("==> " + e);
Result r = smt.checkSat(e);
#include "expr/kind.h"
#include "theory/type_enumerator.h"
#include "util/language.h"
+#include "util/array_store_all.h"
using namespace CVC4;
using namespace CVC4::theory;
void testBooleans() {
TypeEnumerator te(d_nm->booleanType());
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*te, d_nm->mkConst(false));
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(true));
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT( te.isFinished() );
TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT( te.isFinished() );
TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT( te.isFinished() );
}
void testUF() {
void testArith() {
TypeEnumerator te(d_nm->integerType());
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(0)));
for(int i = 1; i <= 100; ++i) {
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(i)));
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-i)));
}
+ TS_ASSERT( ! te.isFinished() );
te = TypeEnumerator(d_nm->realType());
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(0, 1)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 1)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 1)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 1)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 1)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 3)));
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 3)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(4, 1)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-4, 1)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 4)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(5, 1)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-5, 1)));
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 5)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 5)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(6, 1)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(2, 5)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-2, 5)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 6)));
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 6)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(7, 1)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-7, 1)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 5)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 7)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 7)));
+ TS_ASSERT( ! te.isFinished() );
}
void testDatatypesFinite() {
listColors.addConstructor(consC);
listColors.addConstructor(DatatypeConstructor("nil"));
TypeNode listColorsType = TypeNode::fromType(d_em->mkDatatypeType(listColors));
+
TypeEnumerator te(listColorsType);
+ TS_ASSERT( ! te.isFinished() );
Node cons = Node::fromExpr(DatatypeType(listColorsType.toType()).getDatatype().getConstructor("cons"));
Node nil = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(listColorsType.toType()).getDatatype().getConstructor("nil"));
Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("red"));
TS_ASSERT_EQUALS(*te, nil);
TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil));
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)));
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))));
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))));
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))))));
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))))));
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))))))));
+ TS_ASSERT( ! te.isFinished() );
}
- void NOtestDatatypesInfinite2() {
- TypeNode datatype;
- TypeEnumerator te(datatype);
+ void NOTYETtestDatatypesInfinite2() {
+ //TypeNode datatype;
+ //TypeEnumerator te(datatype);
+ //TS_ASSERT( ! te.isFinished() );
TS_FAIL("unimplemented");
}
- void NOtestArraysInfinite() {
+ void testArraysInfinite() {
TypeEnumerator te(d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType()));
+ hash_set<Node, NodeHashFunction> elts;
+ for(size_t i = 0; i < 1000; ++i) {
+ TS_ASSERT( ! te.isFinished() );
+ Node elt = *te++;
+ std::cout << elt << std::endl;
+ // ensure no duplicates
+ TS_ASSERT( elts.find(elt) == elts.end() );
+ elts.insert(elt);
+ }
+ TS_ASSERT( ! te.isFinished() );
- TS_FAIL("unimplemented");
+ // ensure that certain items were found
+ ArrayType arrayType(d_em->mkArrayType(d_em->integerType(), d_em->integerType()));
+ Node zeroes = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(0))));
+ Node ones = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(1))));
+ Node twos = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(2))));
+ Node threes = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(3))));
+ Node fours = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(4))));
+ Node tens = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(10))));
+
+ Node zero = d_nm->mkConst(Rational(0));
+ Node one = d_nm->mkConst(Rational(1));
+ Node two = d_nm->mkConst(Rational(2));
+ Node three = d_nm->mkConst(Rational(3));
+ Node four = d_nm->mkConst(Rational(4));
+ Node five = d_nm->mkConst(Rational(5));
+ Node eleven = d_nm->mkConst(Rational(11));
+
+ // FIXME: the arrays enumerator isn't currently a fair enumerator,
+ // so these will fail; disable them for now
+ //TS_ASSERT( elts.find( d_nm->mkNode(STORE, ones, zero, zero) ) != elts.end() );
+ //TS_ASSERT( elts.find( d_nm->mkNode(STORE, tens, four, five) ) != elts.end() );
+ //TS_ASSERT( elts.find( d_nm->mkNode(STORE, d_nm->mkNode(STORE, d_nm->mkNode(STORE, fours, eleven, two), two, one), zero, two) ) != elts.end() );
+ //TS_ASSERT( elts.find( threes ) != elts.end() );
+ //TS_ASSERT( elts.find( d_nm->mkNode(STORE, d_nm->mkNode(STORE, d_nm->mkNode(STORE, d_nm->mkNode(STORE, twos, three, zero), two, zero), one, zero), zero, zero) ) != elts.end() );
}
- // remove this when ArrayConst is available
- template <class T, class U> inline bool ArrayConst(const T&, const U&) { return false; }
-
- void NOtestArraysFinite() {
- TypeEnumerator te(d_nm->mkArrayType(d_nm->mkBitVectorType(2), d_nm->booleanType()));
- TS_ASSERT_EQUALS(*te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(0)), d_nm->mkConst(false))));
- TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(0)), d_nm->mkConst(true))));
- TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(1)), d_nm->mkConst(false))));
- TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(1)), d_nm->mkConst(true))));
- TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(2)), d_nm->mkConst(false))));
- TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(2)), d_nm->mkConst(true))));
- TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(3)), d_nm->mkConst(false))));
- TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(3)), d_nm->mkConst(true))));
+ void testArraysFinite() {
+ ArrayType arrType(d_em->mkArrayType(d_em->mkBitVectorType(2), d_em->booleanType()));
+ TypeEnumerator te(TypeNode::fromType(arrType));
+ TS_ASSERT( ! te.isFinished() );
+ TS_ASSERT_EQUALS(*te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(false))));
+ TS_ASSERT( ! te.isFinished() );
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(true))));
+ TS_ASSERT( ! te.isFinished() );
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(false))));
+ TS_ASSERT( ! te.isFinished() );
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(true))));
+ TS_ASSERT( ! te.isFinished() );
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(false))));
+ TS_ASSERT( ! te.isFinished() );
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(true))));
+ TS_ASSERT( ! te.isFinished() );
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(false))));
+ TS_ASSERT( ! te.isFinished() );
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(true))));
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT( te.isFinished() );
TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT( te.isFinished() );
TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT( te.isFinished() );
}
void testBV() {
projects / cvc5.git / commitdiff