diff options
Diffstat (limited to 'src')
37 files changed, 1240 insertions, 583 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 3637cb089..c765d325a 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -16,7 +16,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -D __STDC_LIMIT_MACROS \ -D __STDC_FORMAT_MACROS \ - -I@builddir@ -I@srcdir@/include -I@srcdir@ + -I@builddir@ -I@srcdir@/include -I@srcdir@ -I@top_srcdir@/proofs/lfsc_checker AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN) SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main @@ -104,6 +104,7 @@ libcvc4_la_SOURCES = \ prop/sat_solver_registry.cpp \ prop/options_handlers.h \ smt/smt_engine.cpp \ + smt/smt_engine_check_proof.cpp \ smt/smt_engine.h \ smt/model_postprocessor.cpp \ smt/model_postprocessor.h \ @@ -393,6 +394,11 @@ libcvc4_la_LIBADD = \ @builddir@/expr/libexpr.la \ @builddir@/prop/minisat/libminisat.la \ @builddir@/prop/bvminisat/libbvminisat.la +if CVC4_PROOF +libcvc4_la_LIBADD += \ + @top_builddir@/proofs/lfsc_checker/liblfsc_checker.la \ + @top_builddir@/proofs/signatures/libsignatures.la +endif if CVC4_NEEDS_REPLACEMENT_FUNCTIONS libcvc4_la_LIBADD += \ diff --git a/src/cvc4.i b/src/cvc4.i index ec3aa43cb..aadbc374d 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -269,6 +269,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; %include "util/record.i" %include "util/regexp.i" %include "util/uninterpreted_constant.i" +%include "util/proof.i" %include "expr/kind.i" %include "expr/expr.i" diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 467b150d3..485a478d8 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -76,14 +76,20 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) if(q != NULL) { d_result = res = q->getResult(); } - // dump the model if option is set - if( status && - d_options[options::produceModels] && - d_options[options::dumpModels] && - ( res.asSatisfiabilityResult() == Result::SAT || - (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) { - Command* gm = new GetModelCommand(); - status = doCommandSingleton(gm); + // dump the model/proof if option is set + if(status) { + if( d_options[options::produceModels] && + d_options[options::dumpModels] && + ( res.asSatisfiabilityResult() == Result::SAT || + (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) { + Command* gm = new GetModelCommand(); + status = doCommandSingleton(gm); + } else if( d_options[options::proof] && + d_options[options::dumpProofs] && + res.asSatisfiabilityResult() == Result::UNSAT ) { + Command* gp = new GetProofCommand(); + status = doCommandSingleton(gp); + } } return status; } diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 971aa2131..24469c668 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -213,7 +213,6 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) if(d_lastWinner != 0) delete cmdExported; return ret; } else if(mode == 1) { // portfolio - d_seq->addCommand(cmd->clone()); // We currently don't support changing number of threads for each @@ -327,7 +326,26 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) lemmaSharingCleanup(); delete[] fns; - return portfolioReturn.second; + + bool status = portfolioReturn.second; + + // dump the model/proof if option is set + if(status) { + if( d_options[options::produceModels] && + d_options[options::dumpModels] && + ( d_result.asSatisfiabilityResult() == Result::SAT || + (d_result.isUnknown() && d_result.whyUnknown() == Result::INCOMPLETE) ) ) { + Command* gm = new GetModelCommand(); + status = doCommandSingleton(gm); + } else if( d_options[options::proof] && + d_options[options::dumpProofs] && + d_result.asSatisfiabilityResult() == Result::UNSAT ) { + Command* gp = new GetProofCommand(); + status = doCommandSingleton(gp); + } + } + + return status; } else if(mode == 2) { Command* cmdExported = d_lastWinner == 0 ? diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index d1baaa2e9..bf66629dd 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -108,6 +108,10 @@ int runCvc4(int argc, char* argv[], Options& opts) { ! opts[options::threadArgv].empty() ) { throw OptionException("Thread options cannot be used with sequential CVC4. Please build and use the portfolio binary `pcvc4'."); } +# else + if( opts[options::checkProofs] ) { + throw OptionException("Cannot run portfolio in check-proofs mode."); + } # endif progName = opts[options::binary_name].c_str(); @@ -201,8 +205,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { << "Notice: ...the experimental --incremental-parallel option.\n"; exprMgr = new ExprManager(opts); pExecutor = new CommandExecutor(*exprMgr, opts); - } - else { + } else { exprMgr = new ExprManager(threadOpts[0]); pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts); } diff --git a/src/options/mkoptions b/src/options/mkoptions index 65a49afa6..087af0ef6 100755 --- a/src/options/mkoptions +++ b/src/options/mkoptions @@ -241,6 +241,7 @@ function handle_option { predicates= links= links_alternate= + smt_links= options_already_documented=false alternate_options_already_documented=false @@ -412,10 +413,28 @@ function handle_option { links_alternate="${links_alternate} $(echo "${args[$i]}" | sed 's,[^/]*/,,')" else links="${links} ${args[$i]}" - links_alternate="${links_alternate} ${args[$i]}" fi done ;; + :link-smt) + j=0 + while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do + let ++i + let ++j + if [ $j -eq 3 ]; then + echo "$kf:$lineno: error: attribute :link-smt can only take two arguments" >&2 + exit 1 + fi + if expr "${args[$i]}" : '.*/' &>/dev/null; then + echo "$kf:$lineno: error: attribute :link-smt cannot take alternates" >&2 + exit 1 + fi + smt_links="${smt_links} ${args[$i]}" + done + if [ $j -eq 1 ]; then + smt_links="${smt_links} \"true\"" + fi + ;; :include) while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do let ++i @@ -544,14 +563,33 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r fi run_links= run_links_alternate= + run_smt_links= + if [ -n "$links" -a -z "$smt_links" -a -n "$smtname" ]; then + echo "$kf:$lineno: warning: $smtname has no :link-smt, but equivalent command-line has :link" >&2 + elif [ -n "$smt_links" -a -z "$links" ] && [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o "$long_option_alternate" ]; then + echo "$kf:$lineno: warning: $smtname has a :link-smt, but equivalent command-line has no :link" >&2 + fi if [ -n "$links" ]; then + # command-line links for link in $links; do run_links="$run_links #line $lineno \"$kf\" preemptGetopt(extra_argc, extra_argv, \"$link\");" done fi + if [ -n "$smt_links" ]; then + # smt links + smt_links=($smt_links) + i=0 + while [ $i -lt ${#smt_links[@]} ]; do + run_smt_links="$run_smt_links +#line $lineno \"$kf\" + smt->setOption(std::string(\"${smt_links[$i]}\"), SExpr(${smt_links[$(($i+1))]}));" + i=$((i+2)) + done + fi if [ -n "$links_alternate" ]; then + # command-line links for link in $links_alternate; do run_links_alternate="$run_links_alternate #line $lineno \"$kf\" @@ -732,7 +770,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - Options::current().assignBool(options::$internal, \"$smtname\", optionarg == \"true\", smt);$run_links + Options::current().assignBool(options::$internal, \"$smtname\", optionarg == \"true\", smt);$run_smt_links return; }" elif [ -n "$expect_arg" -a "$internal" != - ]; then @@ -749,7 +787,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - Options::current().assign(options::$internal, \"$smtname\", optionarg, smt);$run_links + Options::current().assign(options::$internal, \"$smtname\", optionarg, smt);$run_smt_links return; }" elif [ -n "$expect_arg" ]; then @@ -764,7 +802,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - $run_handlers$run_links + $run_handlers$run_smt_links return; }" else @@ -779,7 +817,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - $run_handlers$run_links + $run_handlers$run_smt_links return; }" fi diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 022c4a069..39329e424 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1252,6 +1252,8 @@ builtinOp[CVC4::Kind& kind] | STRCON_TOK { $kind = CVC4::kind::STRING_CONCAT; } | STRLEN_TOK { $kind = CVC4::kind::STRING_LENGTH; } | STRSUB_TOK { $kind = CVC4::kind::STRING_SUBSTR; } + | STRCTN_TOK { $kind = CVC4::kind::STRING_STRCTN; } + | STRCAT_TOK { $kind = CVC4::kind::STRING_CHARAT; } | STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; } | STRTORE_TOK { $kind = CVC4::kind::STRING_TO_REGEXP; } | RECON_TOK { $kind = CVC4::kind::REGEXP_CONCAT; } @@ -1625,7 +1627,11 @@ INT2BV_TOK : 'int2bv'; //STRCST_TOK : 'str.cst'; STRCON_TOK : 'str.++'; STRLEN_TOK : 'str.len'; -STRSUB_TOK : 'str.sub' ; +STRSUB_TOK : 'str.substr' ; +STRCTN_TOK : 'str.contain' ; +STRCAT_TOK : 'str.at' ; +//STRIDOF_TOK : 'str.indexof' ; +//STRREPL_TOK : 'str.repalce' ; STRINRE_TOK : 'str.in.re'; STRTORE_TOK : 'str.to.re'; RECON_TOK : 're.++'; diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 8ab5c121d..72bfa5603 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -153,6 +153,7 @@ void AstPrinter::toStream(std::ostream& out, const Command* c, tryToStream<GetModelCommand>(out, c) || tryToStream<GetAssignmentCommand>(out, c) || tryToStream<GetAssertionsCommand>(out, c) || + tryToStream<GetProofCommand>(out, c) || tryToStream<SetBenchmarkStatusCommand>(out, c) || tryToStream<SetBenchmarkLogicCommand>(out, c) || tryToStream<SetInfoCommand>(out, c) || @@ -307,6 +308,9 @@ static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() { static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() { out << "GetAssertions()"; } +static void toStream(std::ostream& out, const GetProofCommand* c) throw() { + out << "GetProof()"; +} static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() { out << "SetBenchmarkStatus(" << c->getStatus() << ")"; } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index b0dfbbd67..ca463d10b 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -776,6 +776,7 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, tryToStream<GetModelCommand>(out, c) || tryToStream<GetAssignmentCommand>(out, c) || tryToStream<GetAssertionsCommand>(out, c) || + tryToStream<GetProofCommand>(out, c) || tryToStream<SetBenchmarkStatusCommand>(out, c) || tryToStream<SetBenchmarkLogicCommand>(out, c) || tryToStream<SetInfoCommand>(out, c) || @@ -1031,6 +1032,10 @@ static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() { out << "WHERE;"; } +static void toStream(std::ostream& out, const GetProofCommand* c) throw() { + out << "DUMP_PROOF;"; +} + static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() { out << "% (set-info :status " << c->getStatus() << ")"; } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index b743ba70e..c56d87da6 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -577,6 +577,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, tryToStream<GetModelCommand>(out, c) || tryToStream<GetAssignmentCommand>(out, c) || tryToStream<GetAssertionsCommand>(out, c) || + tryToStream<GetProofCommand>(out, c) || tryToStream<SetBenchmarkStatusCommand>(out, c) || tryToStream<SetBenchmarkLogicCommand>(out, c) || tryToStream<SetInfoCommand>(out, c) || @@ -858,6 +859,10 @@ static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() { out << "(get-assertions)"; } +static void toStream(std::ostream& out, const GetProofCommand* c) throw() { + out << "(get-proof)"; +} + static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() { out << "(set-info :status " << c->getStatus() << ")"; } diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 8e9c4cd21..39e802b62 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -32,37 +32,45 @@ CnfProof::CnfProof(CnfStream* stream) Expr CnfProof::getAtom(prop::SatVariable var) { - prop::SatLiteral lit (var); - Node node = d_cnfStream->getNode(lit); + prop::SatLiteral lit (var); + Node node = d_cnfStream->getNode(lit); Expr atom = node.toExpr(); - return atom; + return atom; } CnfProof::~CnfProof() { } +LFSCCnfProof::iterator LFSCCnfProof::begin_atom_mapping() { + return iterator(*this, ProofManager::currentPM()->begin_vars()); +} + +LFSCCnfProof::iterator LFSCCnfProof::end_atom_mapping() { + return iterator(*this, ProofManager::currentPM()->end_vars()); +} + void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) { ProofManager::var_iterator it = ProofManager::currentPM()->begin_vars(); ProofManager::var_iterator end = ProofManager::currentPM()->end_vars(); - + for (;it != end; ++it) { os << "(decl_atom "; - + if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) { Expr atom = getAtom(*it); - LFSCTheoryProof::printFormula(atom, os); + LFSCTheoryProof::printTerm(atom, os); } else { // print fake atoms for all other logics - os << "true "; + os << "true "; } os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n"; - paren << ")))"; + paren << ")))"; } } void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) { - printInputClauses(os, paren); + printInputClauses(os, paren); printTheoryLemmas(os, paren); } @@ -70,51 +78,49 @@ void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) { os << " ;; Input Clauses \n"; ProofManager::clause_iterator it = ProofManager::currentPM()->begin_input_clauses(); ProofManager::clause_iterator end = ProofManager::currentPM()->end_input_clauses(); - + for (; it != end; ++it) { ClauseId id = it->first; const prop::SatClause* clause = it->second; os << "(satlem _ _ "; - std::ostringstream clause_paren; + std::ostringstream clause_paren; printClause(*clause, os, clause_paren); os << " (clausify_false trust)" << clause_paren.str(); - os << "( \\ " << ProofManager::getInputClauseName(id) << "\n"; - paren << "))"; + os << "( \\ " << ProofManager::getInputClauseName(id) << "\n"; + paren << "))"; } } void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) { - os << " ;; Theory Lemmas \n"; + os << " ;; Theory Lemmas \n"; ProofManager::clause_iterator it = ProofManager::currentPM()->begin_lemmas(); ProofManager::clause_iterator end = ProofManager::currentPM()->end_lemmas(); - + for (; it != end; ++it) { ClauseId id = it->first; const prop::SatClause* clause = it->second; os << "(satlem _ _ "; - std::ostringstream clause_paren; + std::ostringstream clause_paren; printClause(*clause, os, clause_paren); os << " (clausify_false trust)" << clause_paren.str(); - os << "( \\ " << ProofManager::getLemmaClauseName(id) <<"\n"; - paren << "))"; + os << "( \\ " << ProofManager::getLemmaClauseName(id) <<"\n"; + paren << "))"; } } void LFSCCnfProof::printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren) { for (unsigned i = 0; i < clause.size(); ++i) { prop::SatLiteral lit = clause[i]; - prop::SatVariable var = lit.getSatVariable(); + prop::SatVariable var = lit.getSatVariable(); if (lit.isNegated()) { os << "(ast _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " "; - paren << "))"; + paren << "))"; } else { os << "(asf _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " "; - paren << "))"; + paren << "))"; } } } - } /* CVC4 namespace */ - diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 9a2dbe655..0a932f906 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -13,7 +13,7 @@ ** ** A manager for CnfProofs. ** - ** + ** **/ #ifndef __CVC4__CNF_PROOF_H @@ -25,36 +25,68 @@ #include <ext/hash_set> #include <ext/hash_map> -#include <iostream> +#include <iostream> namespace CVC4 { namespace prop { -class CnfStream; + class CnfStream; } +class CnfProof; + +class AtomIterator { + CnfProof& d_cnf; + ProofManager::var_iterator d_it; + +public: + AtomIterator(CnfProof& cnf, const ProofManager::var_iterator& it) + : d_cnf(cnf), d_it(it) + {} + inline Expr operator*(); + AtomIterator& operator++() { ++d_it; return *this; } + AtomIterator operator++(int) { AtomIterator x = *this; ++d_it; return x; } + bool operator==(const AtomIterator& it) const { return &d_cnf == &it.d_cnf && d_it == it.d_it; } + bool operator!=(const AtomIterator& it) const { return !(*this == it); } +};/* class AtomIterator */ + class CnfProof { protected: CVC4::prop::CnfStream* d_cnfStream; Expr getAtom(prop::SatVariable var); + friend class AtomIterator; public: CnfProof(CVC4::prop::CnfStream* cnfStream); + typedef AtomIterator iterator; + virtual iterator begin_atom_mapping() = 0; + virtual iterator end_atom_mapping() = 0; + virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0; virtual void printClauses(std::ostream& os, std::ostream& paren) = 0; - virtual ~CnfProof(); + virtual ~CnfProof(); }; -class LFSCCnfProof: public CnfProof { +class LFSCCnfProof : public CnfProof { void printInputClauses(std::ostream& os, std::ostream& paren); void printTheoryLemmas(std::ostream& os, std::ostream& paren); void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren); + public: LFSCCnfProof(CVC4::prop::CnfStream* cnfStream) : CnfProof(cnfStream) {} + + virtual iterator begin_atom_mapping(); + virtual iterator end_atom_mapping(); + virtual void printAtomMapping(std::ostream& os, std::ostream& paren); virtual void printClauses(std::ostream& os, std::ostream& paren); }; +inline Expr AtomIterator::operator*() { + return d_cnf.getAtom(*d_it); +} + } /* CVC4 namespace */ + #endif /* __CVC4__CNF_PROOF_H */ diff --git a/src/proof/proof.h b/src/proof/proof.h index 02f8f7684..e3b776cce 100644 --- a/src/proof/proof.h +++ b/src/proof/proof.h @@ -23,7 +23,7 @@ #ifdef CVC4_PROOF # define PROOF(x) if(options::proof()) { x; } -# define NULLPROOF(x) (options::proof())? x : NULL +# define NULLPROOF(x) (options::proof()) ? x : NULL # define PROOF_ON() options::proof() #else /* CVC4_PROOF */ # define PROOF(x) diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 110e6b79a..14a82b17b 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -28,14 +28,10 @@ namespace CVC4 { std::string append(const std::string& str, uint64_t num) { std::ostringstream os; - os << str << num; - return os.str(); + os << str << num; + return os.str(); } - -bool ProofManager::isInitialized = false; -ProofManager* ProofManager::proofManager = NULL; - ProofManager::ProofManager(ProofFormat format): d_satProof(NULL), d_cnfProof(NULL), @@ -50,41 +46,43 @@ ProofManager::~ProofManager() { delete d_cnfProof; delete d_theoryProof; delete d_fullProof; - for (IdToClause::iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) { - delete it->second; + + for(IdToClause::iterator it = d_inputClauses.begin(); + it != d_inputClauses.end(); + ++it) { + delete it->second; } - for (IdToClause::iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) { - delete it->second; + + for(IdToClause::iterator it = d_theoryLemmas.begin(); + it != d_theoryLemmas.end(); + ++it) { + delete it->second; } - // FIXME: memory leak because there are deleted theory lemmas that were not used in the - // SatProof + + // FIXME: memory leak because there are deleted theory lemmas that + // were not used in the SatProof } ProofManager* ProofManager::currentPM() { - if (isInitialized) { - return proofManager; - } else { - proofManager = new ProofManager(); - isInitialized = true; - return proofManager; - } + return smt::currentProofManager(); } Proof* ProofManager::getProof(SmtEngine* smt) { - if (currentPM()->d_fullProof != NULL) + if (currentPM()->d_fullProof != NULL) { return currentPM()->d_fullProof; + } Assert (currentPM()->d_format == LFSC); currentPM()->d_fullProof = new LFSCProof(smt, (LFSCSatProof*)getSatProof(), (LFSCCnfProof*)getCnfProof(), - (LFSCTheoryProof*)getTheoryProof()); + (LFSCTheoryProof*)getTheoryProof()); return currentPM()->d_fullProof; } SatProof* ProofManager::getSatProof() { Assert (currentPM()->d_satProof); - return currentPM()->d_satProof; + return currentPM()->d_satProof; } CnfProof* ProofManager::getCnfProof() { @@ -107,7 +105,7 @@ void ProofManager::initSatProof(Minisat::Solver* solver) { void ProofManager::initCnfProof(prop::CnfStream* cnfStream) { Assert (currentPM()->d_cnfProof == NULL); Assert (currentPM()->d_format == LFSC); - currentPM()->d_cnfProof = new LFSCCnfProof(cnfStream); + currentPM()->d_cnfProof = new LFSCCnfProof(cnfStream); } void ProofManager::initTheoryProof() { @@ -126,8 +124,8 @@ std::string ProofManager::getLitName(prop::SatLiteral lit) {return append("l", l void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) { for (unsigned i = 0; i < clause->size(); ++i) { - prop::SatLiteral lit = clause->operator[](i); - d_propVars.insert(lit.getSatVariable()); + prop::SatLiteral lit = clause->operator[](i); + d_propVars.insert(lit.getSatVariable()); } if (kind == INPUT) { d_inputClauses.insert(std::make_pair(id, clause)); @@ -138,11 +136,11 @@ void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseK } void ProofManager::addAssertion(Expr formula) { - d_inputFormulas.insert(formula); + d_inputFormulas.insert(formula); } void ProofManager::setLogic(const std::string& logic_string) { - d_logic = logic_string; + d_logic = logic_string; } @@ -158,17 +156,24 @@ LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, void LFSCProof::toStream(std::ostream& out) { smt::SmtScope scope(d_smtEngine); std::ostringstream paren; - out << "(check \n"; - if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) { - d_theoryProof->printAssertions(out, paren); + out << "(check\n"; + if (d_theoryProof == NULL) { + d_theoryProof = new LFSCTheoryProof(); + } + for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping(); + i != d_cnfProof->end_atom_mapping(); + ++i) { + d_theoryProof->addDeclaration(*i); } - out << "(: (holds cln) \n"; + d_theoryProof->printAssertions(out, paren); + out << "(: (holds cln)\n"; d_cnfProof->printAtomMapping(out, paren); d_cnfProof->printClauses(out, paren); - d_satProof->printResolutions(out, paren); + d_satProof->printResolutions(out, paren); paren <<")))\n;;"; - out << paren.str(); + out << paren.str(); + out << "\n"; } -} /* CVC4 namespace */ +} /* CVC4 namespace */ diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index e33f1a63f..ab8a7b2bc 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -9,11 +9,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief A manager for Proofs. + ** \brief A manager for Proofs ** ** A manager for Proofs. - ** - ** **/ #include "cvc4_private.h" @@ -21,7 +19,7 @@ #ifndef __CVC4__PROOF_MANAGER_H #define __CVC4__PROOF_MANAGER_H -#include <iostream> +#include <iostream> #include "proof/proof.h" #include "util/proof.h" @@ -29,15 +27,15 @@ // forward declarations namespace Minisat { class Solver; -} +}/* Minisat namespace */ namespace CVC4 { namespace prop { class CnfStream; -} +}/* CVC4::prop namespace */ -class SmtEngine; +class SmtEngine; typedef int ClauseId; @@ -51,10 +49,10 @@ class LFSCCnfProof; class LFSCTheoryProof; namespace prop { -typedef uint64_t SatVariable; -class SatLiteral; -typedef std::vector<SatLiteral> SatClause; -} + typedef uint64_t SatVariable; + class SatLiteral; + typedef std::vector<SatLiteral> SatClause; +}/* CVC4::prop namespace */ // different proof modes enum ProofFormat { @@ -64,7 +62,7 @@ enum ProofFormat { std::string append(const std::string& str, uint64_t num); -typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause; +typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause; typedef __gnu_cxx::hash_set<prop::SatVariable > VarSet; typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; @@ -74,35 +72,36 @@ enum ClauseKind { INPUT, THEORY_LEMMA, LEARNT -}; +};/* enum ClauseKind */ class ProofManager { SatProof* d_satProof; CnfProof* d_cnfProof; - TheoryProof* d_theoryProof; + TheoryProof* d_theoryProof; // information that will need to be shared across proofs IdToClause d_inputClauses; IdToClause d_theoryLemmas; ExprSet d_inputFormulas; VarSet d_propVars; - - Proof* d_fullProof; + + Proof* d_fullProof; ProofFormat d_format; - - static ProofManager* proofManager; - static bool isInitialized; - ProofManager(ProofFormat format = LFSC); - ~ProofManager(); + protected: std::string d_logic; + public: + ProofManager(ProofFormat format = LFSC); + ~ProofManager(); + static ProofManager* currentPM(); - // initialization - static void initSatProof(Minisat::Solver* solver); + + // initialization + static void initSatProof(Minisat::Solver* solver); static void initCnfProof(CVC4::prop::CnfStream* cnfStream); static void initTheoryProof(); - + static Proof* getProof(SmtEngine* smt); static SatProof* getSatProof(); static CnfProof* getCnfProof(); @@ -110,9 +109,9 @@ public: // iterators over data shared by proofs typedef IdToClause::const_iterator clause_iterator; - typedef ExprSet::const_iterator assertions_iterator; + typedef ExprSet::const_iterator assertions_iterator; typedef VarSet::const_iterator var_iterator; - + clause_iterator begin_input_clauses() const { return d_inputClauses.begin(); } clause_iterator end_input_clauses() const { return d_inputClauses.end(); } @@ -124,10 +123,10 @@ public: var_iterator begin_vars() const { return d_propVars.begin(); } var_iterator end_vars() const { return d_propVars.end(); } - + void addAssertion(Expr formula); - void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); - + void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); + // variable prefixes static std::string getInputClauseName(ClauseId id); static std::string getLemmaClauseName(ClauseId id); @@ -136,7 +135,7 @@ public: static std::string getVarName(prop::SatVariable var); static std::string getAtomName(prop::SatVariable var); static std::string getLitName(prop::SatLiteral lit); - + void setLogic(const std::string& logic_string); const std::string getLogic() const { return d_logic; } };/* class ProofManager */ @@ -145,13 +144,13 @@ class LFSCProof : public Proof { LFSCSatProof* d_satProof; LFSCCnfProof* d_cnfProof; LFSCTheoryProof* d_theoryProof; - SmtEngine* d_smtEngine; + SmtEngine* d_smtEngine; public: - LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory); + LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory); virtual void toStream(std::ostream& out); virtual ~LFSCProof() {} -}; - +};/* class LFSCProof */ + }/* CVC4 namespace */ #endif /* __CVC4__PROOF_MANAGER_H */ diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index da9df0d42..3b5509ffb 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -25,7 +25,7 @@ using namespace Minisat; using namespace CVC4::prop; namespace CVC4 { -/// some helper functions +/// some helper functions void printLit (Minisat::Lit l) { Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1; @@ -33,16 +33,16 @@ void printLit (Minisat::Lit l) { void printClause (Minisat::Clause& c) { for (int i = 0; i < c.size(); i++) { - Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; + Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; } } void printLitSet(const LitSet& s) { for(LitSet::iterator it = s.begin(); it != s.end(); ++it) { printLit(*it); - Debug("proof:sat") << " "; + Debug("proof:sat") << " "; } - Debug("proof:sat") << endl; + Debug("proof:sat") << endl; } // purely debugging functions @@ -52,39 +52,38 @@ void printDebug (Minisat::Lit l) { void printDebug (Minisat::Clause& c) { for (int i = 0; i < c.size(); i++) { - Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; + Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; } Debug("proof:sat") << endl; } -int SatProof::d_idCounter = 0; +int SatProof::d_idCounter = 0; -/** +/** * Converts the clause associated to id to a set of literals - * + * * @param id the clause id - * @param set the clause converted to a set of literals + * @param set the clause converted to a set of literals */ void SatProof::createLitSet(ClauseId id, LitSet& set) { - Assert (set.empty()); + Assert(set.empty()); if(isUnit(id)) { set.insert(getUnit(id)); return; } if ( id == d_emptyClauseId) { - return; + return; } CRef ref = getClauseRef(id); - Assert (ref != CRef_Undef); - Clause& c = d_solver->ca[ref]; + Clause& c = getClause(ref); for (int i = 0; i < c.size(); i++) { - set.insert(c[i]); + set.insert(c[i]); } } -/** +/** * Resolves clause1 and clause2 on variable var and stores the * result in clause1 * @param v @@ -93,36 +92,40 @@ void SatProof::createLitSet(ClauseId id, LitSet& set) { */ bool resolve(const Lit v, LitSet& clause1, LitSet& clause2, bool s) { Assert(!clause1.empty()); - Assert(!clause2.empty()); - Lit var = sign(v) ? ~v : v; + Assert(!clause2.empty()); + Lit var = sign(v) ? ~v : v; if (s) { // literal appears positive in the first clause if( !clause2.count(~var)) { - Debug("proof:sat") << "proof:resolve: Missing literal "; - printLit(var); - Debug("proof:sat") << endl; - return false; + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:resolve: Missing literal "; + printLit(var); + Debug("proof:sat") << endl; + } + return false; } clause1.erase(var); clause2.erase(~var); for (LitSet::iterator it = clause2.begin(); it!= clause2.end(); ++it) { - clause1.insert(*it); + clause1.insert(*it); } } else { // literal appears negative in the first clause if( !clause1.count(~var) || !clause2.count(var)) { - Debug("proof:sat") << "proof:resolve: Missing literal "; - printLit(var); - Debug("proof:sat") << endl; - return false; + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:resolve: Missing literal "; + printLit(var); + Debug("proof:sat") << endl; + } + return false; } clause1.erase(~var); clause2.erase(var); for (LitSet::iterator it = clause2.begin(); it!= clause2.end(); ++it) { - clause1.insert(*it); + clause1.insert(*it); } } - return true; + return true; } /// ResChain @@ -135,16 +138,16 @@ ResChain::ResChain(ClauseId start) : void ResChain::addStep(Lit lit, ClauseId id, bool sign) { ResStep step(lit, id, sign); - d_steps.push_back(step); + d_steps.push_back(step); } void ResChain::addRedundantLit(Lit lit) { if (d_redundantLits) { - d_redundantLits->insert(lit); + d_redundantLits->insert(lit); } else { d_redundantLits = new LitSet(); - d_redundantLits->insert(lit); + d_redundantLits->insert(lit); } } @@ -156,7 +159,7 @@ ProofProxy::ProofProxy(SatProof* proof): {} void ProofProxy::updateCRef(CRef oldref, CRef newref) { - d_proof->updateCRef(oldref, newref); + d_proof->updateCRef(oldref, newref); } @@ -183,27 +186,27 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) : d_seenInput(), d_seenLemmas() { - d_proxy = new ProofProxy(this); + d_proxy = new ProofProxy(this); } -/** +/** * Returns true if the resolution chain corresponding to id * does resolve to the clause associated to id - * @param id - * - * @return + * @param id + * + * @return */ bool SatProof::checkResolution(ClauseId id) { if(d_checkRes) { - bool validRes = true; - Assert (d_resChains.find(id) != d_resChains.end()); + bool validRes = true; + Assert(d_resChains.find(id) != d_resChains.end()); ResChain* res = d_resChains[id]; LitSet clause1; createLitSet(res->getStart(), clause1); - ResSteps& steps = res->getSteps(); + ResSteps& steps = res->getSteps(); for (unsigned i = 0; i < steps.size(); i++) { Lit var = steps[i].lit; - LitSet clause2; + LitSet clause2; createLitSet (steps[i].id, clause2); bool res = resolve (var, clause1, clause2, steps[i].sign); if(res == false) { @@ -215,35 +218,38 @@ bool SatProof::checkResolution(ClauseId id) { if (isUnit(id)) { // special case if it was a unit clause Lit unit = getUnit(id); - validRes = clause1.size() == clause1.count(unit) && !clause1.empty(); - return validRes; + validRes = clause1.size() == clause1.count(unit) && !clause1.empty(); + return validRes; } if (id == d_emptyClauseId) { - return clause1.empty(); + return clause1.empty(); } CRef ref = getClauseRef(id); - Assert (ref != CRef_Undef); - Clause& c = d_solver->ca[ref]; + Clause& c = getClause(ref); for (int i = 0; i < c.size(); ++i) { int count = clause1.erase(c[i]); if (count == 0) { - Debug("proof:sat") << "proof:checkResolution::literal not in computed result "; - printLit(c[i]); - Debug("proof:sat") << "\n"; - validRes = false; + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:checkResolution::literal not in computed result "; + printLit(c[i]); + Debug("proof:sat") << "\n"; + } + validRes = false; } } validRes = clause1.empty(); if (! validRes) { - Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, unremoved literals: \n"; - printLitSet(clause1); - Debug("proof:sat") << "proof:checkResolution:: result should be: \n"; - printClause(c); + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, unremoved literals: \n"; + printLitSet(clause1); + Debug("proof:sat") << "proof:checkResolution:: result should be: \n"; + printClause(c); + } } - return validRes; - + return validRes; + } else { - return true; + return true; } } @@ -254,16 +260,16 @@ bool SatProof::checkResolution(ClauseId id) { ClauseId SatProof::getClauseId(::Minisat::CRef ref) { if(d_clauseId.find(ref) == d_clauseId.end()) { - Debug("proof:sat") << "Missing clause \n"; + Debug("proof:sat") << "Missing clause \n"; } Assert(d_clauseId.find(ref) != d_clauseId.end()); - return d_clauseId[ref]; + return d_clauseId[ref]; } ClauseId SatProof::getClauseId(::Minisat::Lit lit) { Assert(d_unitId.find(toInt(lit)) != d_unitId.end()); - return d_unitId[toInt(lit)]; + return d_unitId[toInt(lit)]; } Minisat::CRef SatProof::getClauseRef(ClauseId id) { @@ -273,79 +279,85 @@ Minisat::CRef SatProof::getClauseRef(ClauseId id) { << (isUnit(id)? "Unit" : "") << endl; } Assert(d_idClause.find(id) != d_idClause.end()); - return d_idClause[id]; + return d_idClause[id]; } Clause& SatProof::getClause(CRef ref) { - return d_solver->ca[ref]; + Assert(ref != CRef_Undef); + Assert(ref >= 0 && ref < d_solver->ca.size()); + return d_solver->ca[ref]; } + Minisat::Lit SatProof::getUnit(ClauseId id) { - Assert (d_idUnit.find(id) != d_idUnit.end()); - return d_idUnit[id]; + Assert(d_idUnit.find(id) != d_idUnit.end()); + return d_idUnit[id]; } bool SatProof::isUnit(ClauseId id) { - return d_idUnit.find(id) != d_idUnit.end(); + return d_idUnit.find(id) != d_idUnit.end(); } bool SatProof::isUnit(::Minisat::Lit lit) { - return d_unitId.find(toInt(lit)) != d_unitId.end(); + return d_unitId.find(toInt(lit)) != d_unitId.end(); } ClauseId SatProof::getUnitId(::Minisat::Lit lit) { - Assert(isUnit(lit)); - return d_unitId[toInt(lit)]; + Assert(isUnit(lit)); + return d_unitId[toInt(lit)]; } bool SatProof::hasResolution(ClauseId id) { - return d_resChains.find(id) != d_resChains.end(); + return d_resChains.find(id) != d_resChains.end(); } bool SatProof::isInputClause(ClauseId id) { - return (d_inputClauses.find(id) != d_inputClauses.end()); + return (d_inputClauses.find(id) != d_inputClauses.end()); } bool SatProof::isLemmaClause(ClauseId id) { - return (d_lemmaClauses.find(id) != d_lemmaClauses.end()); + return (d_lemmaClauses.find(id) != d_lemmaClauses.end()); } void SatProof::print(ClauseId id) { if (d_deleted.find(id) != d_deleted.end()) { - Debug("proof:sat") << "del"<<id; + Debug("proof:sat") << "del"<<id; } else if (isUnit(id)) { - printLit(getUnit(id)); + printLit(getUnit(id)); } else if (id == d_emptyClauseId) { - Debug("proof:sat") << "empty "<< endl; + Debug("proof:sat") << "empty "<< endl; } else { - CRef ref = getClauseRef(id); - Assert (ref != CRef_Undef); - printClause(d_solver->ca[ref]); + CRef ref = getClauseRef(id); + printClause(getClause(ref)); } } void SatProof::printRes(ClauseId id) { Assert(hasResolution(id)); Debug("proof:sat") << "id "<< id <<": "; - printRes(d_resChains[id]); + printRes(d_resChains[id]); } void SatProof::printRes(ResChain* res) { ClauseId start_id = res->getStart(); - Debug("proof:sat") << "("; - print(start_id); + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "("; + print(start_id); + } ResSteps& steps = res->getSteps(); for(unsigned i = 0; i < steps.size(); i++ ) { Lit v = steps[i].lit; ClauseId id = steps[i].id; - Debug("proof:sat") << "["; - printLit(v); - Debug("proof:sat") << "] "; - print(id); + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "["; + printLit(v); + Debug("proof:sat") << "] "; + print(id); + } } Debug("proof:sat") << ") \n"; } @@ -353,23 +365,23 @@ void SatProof::printRes(ResChain* res) { /// registration methods ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind) { - Assert(clause != CRef_Undef); + Assert(clause != CRef_Undef); ClauseIdMap::iterator it = d_clauseId.find(clause); - if (it == d_clauseId.end()) { - ClauseId newId = d_idCounter++; - d_clauseId[clause]= newId; - d_idClause[newId] =clause; - if (kind == INPUT) { - Assert (d_inputClauses.find(newId) == d_inputClauses.end()); - d_inputClauses.insert(newId); - } - if (kind == THEORY_LEMMA) { - Assert (d_lemmaClauses.find(newId) == d_lemmaClauses.end()); - d_lemmaClauses.insert(newId); - } - } - Debug("proof:sat:detailed") <<"registerClause CRef:" << clause <<" id:" << d_clauseId[clause] << " " << kind << "\n"; - return d_clauseId[clause]; + if (it == d_clauseId.end()) { + ClauseId newId = d_idCounter++; + d_clauseId[clause] = newId; + d_idClause[newId] = clause; + if (kind == INPUT) { + Assert(d_inputClauses.find(newId) == d_inputClauses.end()); + d_inputClauses.insert(newId); + } + if (kind == THEORY_LEMMA) { + Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); + d_lemmaClauses.insert(newId); + } + } + Debug("proof:sat:detailed") <<"registerClause CRef:" << clause <<" id:" << d_clauseId[clause] << " " << kind << "\n"; + return d_clauseId[clause]; } ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) { @@ -377,44 +389,42 @@ ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) { if (it == d_unitId.end()) { ClauseId newId = d_idCounter++; d_unitId[toInt(lit)] = newId; - d_idUnit[newId] = lit; + d_idUnit[newId] = lit; if (kind == INPUT) { - Assert (d_inputClauses.find(newId) == d_inputClauses.end()); - d_inputClauses.insert(newId); + Assert(d_inputClauses.find(newId) == d_inputClauses.end()); + d_inputClauses.insert(newId); } if (kind == THEORY_LEMMA) { - Assert (d_lemmaClauses.find(newId) == d_lemmaClauses.end()); - d_lemmaClauses.insert(newId); + Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); + d_lemmaClauses.insert(newId); } - } - Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n"; - return d_unitId[toInt(lit)]; + Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n"; + return d_unitId[toInt(lit)]; } void SatProof::removedDfs(::Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen) { // if we already added the literal return if (seen.count(lit)) { - return; + return; } CRef reason_ref = d_solver->reason(var(lit)); if (reason_ref == CRef_Undef) { seen.insert(lit); - removeStack.push_back(lit); - return; + removeStack.push_back(lit); + return; } - Assert (reason_ref != CRef_Undef); - int size = d_solver->ca[reason_ref].size(); + int size = getClause(reason_ref).size(); for (int i = 1; i < size; i++ ) { - Lit v = d_solver->ca[reason_ref][i]; + Lit v = getClause(reason_ref)[i]; if(inClause.count(v) == 0 && seen.count(v) == 0) { removedDfs(v, removedSet, removeStack, inClause, seen); } } if(seen.count(lit) == 0) { - seen.insert(lit); + seen.insert(lit); removeStack.push_back(lit); } } @@ -427,39 +437,41 @@ void SatProof::removeRedundantFromRes(ResChain* res, ClauseId id) { } LitSet inClause; - createLitSet(id, inClause); - + createLitSet(id, inClause); + LitVector removeStack; - LitSet seen; + LitSet seen; for (LitSet::iterator it = removed->begin(); it != removed->end(); ++it) { - removedDfs(*it, removed, removeStack, inClause, seen); + removedDfs(*it, removed, removeStack, inClause, seen); } - + for (int i = removeStack.size()-1; i >= 0; --i) { Lit lit = removeStack[i]; CRef reason_ref = d_solver->reason(var(lit)); - ClauseId reason_id; + ClauseId reason_id; if (reason_ref == CRef_Undef) { Assert(isUnit(~lit)); - reason_id = getUnitId(~lit); + reason_id = getUnitId(~lit); } else { reason_id = registerClause(reason_ref); } res->addStep(lit, reason_id, !sign(lit)); } - removed->clear(); + removed->clear(); } void SatProof::registerResolution(ClauseId id, ResChain* res) { Assert(res != NULL); removeRedundantFromRes(res, id); - Assert(res->redundantRemoved()); + Assert(res->redundantRemoved()); d_resChains[id] = res; - printRes(id); - if (d_checkRes) { + if(Debug.isOn("proof:sat")) { + printRes(id); + } + if(d_checkRes) { Assert(checkResolution(id)); } } @@ -468,48 +480,46 @@ void SatProof::registerResolution(ClauseId id, ResChain* res) { /// recording resolutions void SatProof::startResChain(::Minisat::CRef start) { - ClauseId id = getClauseId(start); + ClauseId id = getClauseId(start); ResChain* res = new ResChain(id); - d_resStack.push_back(res); + d_resStack.push_back(res); } void SatProof::addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign) { ClauseId id = registerClause(clause); ResChain* res = d_resStack.back(); - res->addStep(lit, id, sign); + res->addStep(lit, id, sign); } void SatProof::endResChain(CRef clause) { Assert(d_resStack.size() > 0); - ClauseId id = registerClause(clause); + ClauseId id = registerClause(clause); ResChain* res = d_resStack.back(); registerResolution(id, res); - d_resStack.pop_back(); + d_resStack.pop_back(); } void SatProof::endResChain(::Minisat::Lit lit) { Assert(d_resStack.size() > 0); - ClauseId id = registerUnitClause(lit); + ClauseId id = registerUnitClause(lit); ResChain* res = d_resStack.back(); - - registerResolution(id, res); - d_resStack.pop_back(); + d_resStack.pop_back(); } void SatProof::storeLitRedundant(::Minisat::Lit lit) { Assert(d_resStack.size() > 0); ResChain* res = d_resStack.back(); - res->addRedundantLit(lit); + res->addRedundantLit(lit); } -/// constructing resolutions +/// constructing resolutions void SatProof::resolveOutUnit(::Minisat::Lit lit) { ClauseId id = resolveUnit(~lit); ResChain* res = d_resStack.back(); - res->addStep(lit, id, !sign(lit)); + res->addStep(lit, id, !sign(lit)); } void SatProof::storeUnitResolution(::Minisat::Lit lit) { @@ -520,28 +530,30 @@ ClauseId SatProof::resolveUnit(::Minisat::Lit lit) { // first check if we already have a resolution for lit if(isUnit(lit)) { ClauseId id = getClauseId(lit); - if(hasResolution(id) || isInputClause(id)) { - return id; - } - Assert (false); + Assert(hasResolution(id) || isInputClause(id) || isLemmaClause(id)); + return id; } CRef reason_ref = d_solver->reason(var(lit)); - Assert (reason_ref != CRef_Undef); - - ClauseId reason_id = registerClause(reason_ref); - - ResChain* res = new ResChain(reason_id); - Clause& reason = d_solver->ca[reason_ref]; - for (int i = 0; i < reason.size(); i++) { - Lit l = reason[i]; - if(lit != l) { + Assert(reason_ref != CRef_Undef); + + ClauseId reason_id = registerClause(reason_ref); + + ResChain* res = new ResChain(reason_id); + // Here, the call to resolveUnit() can reallocate memory in the + // clause allocator. So reload reason ptr each time. + Clause* reason = &getClause(reason_ref); + for (int i = 0; + i < reason->size(); + i++, reason = &getClause(reason_ref)) { + Lit l = (*reason)[i]; + if(lit != l) { ClauseId res_id = resolveUnit(~l); res->addStep(l, res_id, !sign(l)); } } - ClauseId unit_id = registerUnitClause(lit); + ClauseId unit_id = registerUnitClause(lit); registerResolution(unit_id, res); - return unit_id; + return unit_id; } void SatProof::toStream(std::ostream& out) { @@ -549,50 +561,62 @@ void SatProof::toStream(std::ostream& out) { Unimplemented("native proof printing not supported yet"); } -void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit) { - Assert (!d_storedUnitConflict); - d_unitConflictId = registerUnitClause(conflict_lit); +void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind) { + Assert(!d_storedUnitConflict); + d_unitConflictId = registerUnitClause(conflict_lit, kind); d_storedUnitConflict = true; - Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n"; + Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n"; } void SatProof::finalizeProof(::Minisat::CRef conflict_ref) { Assert(d_resStack.size() == 0); - Assert (conflict_ref != ::Minisat::CRef_Undef); - ClauseId conflict_id; + Assert(conflict_ref != ::Minisat::CRef_Undef); + ClauseId conflict_id; if (conflict_ref == ::Minisat::CRef_Lazy) { - Assert (d_storedUnitConflict); - conflict_id = d_unitConflictId; + Assert(d_storedUnitConflict); + conflict_id = d_unitConflictId; + + ResChain* res = new ResChain(conflict_id); + Lit lit = d_idUnit[conflict_id]; + ClauseId res_id = resolveUnit(~lit); + res->addStep(lit, res_id, !sign(lit)); + + registerResolution(d_emptyClauseId, res); + + return; } else { - Assert (!d_storedUnitConflict); + Assert(!d_storedUnitConflict); conflict_id = registerClause(conflict_ref); //FIXME } - Debug("proof:sat") << "proof::finalizeProof Final Conflict "; - print(conflict_id); - + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof::finalizeProof Final Conflict "; + print(conflict_id); + } + ResChain* res = new ResChain(conflict_id); - Clause& conflict = d_solver->ca[conflict_ref] ; - for (int i = 0; i < conflict.size(); ++i) { - Lit lit = conflict[i]; + // Here, the call to resolveUnit() can reallocate memory in the + // clause allocator. So reload conflict ptr each time. + Clause* conflict = &getClause(conflict_ref); + for (int i = 0; + i < conflict->size(); + ++i, conflict = &getClause(conflict_ref)) { + Lit lit = (*conflict)[i]; ClauseId res_id = resolveUnit(~lit); - res->addStep(lit, res_id, !sign(lit)); + res->addStep(lit, res_id, !sign(lit)); } registerResolution(d_emptyClauseId, res); - // // FIXME: massive hack - // Proof* proof = ProofManager::getProof(); - // proof->toStream(std::cout); } /// CRef manager void SatProof::updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref) { if (d_clauseId.find(oldref) == d_clauseId.end()) { - return; + return; } ClauseId id = getClauseId(oldref); - Assert (d_temp_clauseId.find(newref) == d_temp_clauseId.end()); - Assert (d_temp_idClause.find(id) == d_temp_idClause.end()); + Assert(d_temp_clauseId.find(newref) == d_temp_clauseId.end()); + Assert(d_temp_idClause.find(id) == d_temp_idClause.end()); d_temp_clauseId[newref] = id; d_temp_idClause[id] = newref; } @@ -602,39 +626,39 @@ void SatProof::finishUpdateCRef() { d_temp_clauseId.clear(); d_idClause.swap(d_temp_idClause); - d_temp_idClause.clear(); + d_temp_idClause.clear(); } void SatProof::markDeleted(CRef clause) { if (d_clauseId.find(clause) != d_clauseId.end()) { ClauseId id = getClauseId(clause); - Assert (d_deleted.find(id) == d_deleted.end()); + Assert(d_deleted.find(id) == d_deleted.end()); d_deleted.insert(id); if (isLemmaClause(id)) { const Clause& minisat_cl = getClause(clause); - SatClause* sat_cl = new SatClause(); - MinisatSatSolver::toSatClause(minisat_cl, *sat_cl); - d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl)); + SatClause* sat_cl = new SatClause(); + MinisatSatSolver::toSatClause(minisat_cl, *sat_cl); + d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl)); } } } void SatProof::constructProof() { - collectClauses(d_emptyClauseId); + collectClauses(d_emptyClauseId); } std::string SatProof::clauseName(ClauseId id) { ostringstream os; if (isInputClause(id)) { - os << ProofManager::getInputClauseName(id); - return os.str(); - } else + os << ProofManager::getInputClauseName(id); + return os.str(); + } else if (isLemmaClause(id)) { - os << ProofManager::getLemmaClauseName(id); - return os.str(); + os << ProofManager::getLemmaClauseName(id); + return os.str(); }else { os << ProofManager::getLearntClauseName(id); - return os.str(); + return os.str(); } } @@ -643,58 +667,56 @@ void SatProof::addToProofManager(ClauseId id, ClauseKind kind) { Minisat::Lit lit = getUnit(id); prop::SatLiteral sat_lit = MinisatSatSolver::toSatLiteral(lit); prop::SatClause* clause = new SatClause(); - clause->push_back(sat_lit); - ProofManager::currentPM()->addClause(id, clause, kind); - return; + clause->push_back(sat_lit); + ProofManager::currentPM()->addClause(id, clause, kind); + return; } - + if (isDeleted(id)) { - Assert (kind == THEORY_LEMMA); + Assert(kind == THEORY_LEMMA); SatClause* clause = d_deletedTheoryLemmas.find(id)->second; - ProofManager::currentPM()->addClause(id, clause, kind); - return; + ProofManager::currentPM()->addClause(id, clause, kind); + return; } - + CRef ref = getClauseRef(id); const Clause& minisat_cl = getClause(ref); SatClause* clause = new SatClause(); - MinisatSatSolver::toSatClause(minisat_cl, *clause); - ProofManager::currentPM()->addClause(id, clause, kind); + MinisatSatSolver::toSatClause(minisat_cl, *clause); + ProofManager::currentPM()->addClause(id, clause, kind); } void SatProof::collectClauses(ClauseId id) { if (d_seenLearnt.find(id) != d_seenLearnt.end()) { - return; + return; } if (d_seenInput.find(id) != d_seenInput.end()) { - return; + return; } if (d_seenLemmas.find(id) != d_seenLemmas.end()) { - return; + return; } if (isInputClause(id)) { - addToProofManager(id, INPUT); + addToProofManager(id, INPUT); d_seenInput.insert(id); - return; - } - else if (isLemmaClause(id)) { - addToProofManager(id, THEORY_LEMMA); + return; + } else if (isLemmaClause(id)) { + addToProofManager(id, THEORY_LEMMA); d_seenLemmas.insert(id); - return; - } - else { - d_seenLearnt.insert(id); + return; + } else { + d_seenLearnt.insert(id); } - Assert (d_resChains.find(id) != d_resChains.end()); + Assert(d_resChains.find(id) != d_resChains.end()); ResChain* res = d_resChains[id]; ClauseId start = res->getStart(); collectClauses(start); - ResSteps steps = res->getSteps(); - for(unsigned i = 0; i < steps.size(); i++) { - collectClauses(steps[i].id); + ResSteps steps = res->getSteps(); + for(size_t i = 0; i < steps.size(); i++) { + collectClauses(steps[i].id); } } @@ -703,29 +725,29 @@ void SatProof::collectClauses(ClauseId id) { void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) { out << "(satlem_simplify _ _ _ "; - ResChain* res = d_resChains[id]; + ResChain* res = d_resChains[id]; ResSteps& steps = res->getSteps(); - + for (int i = steps.size()-1; i >= 0; i--) { out << "("; out << (steps[i].sign? "R" : "Q") << " _ _ "; - + } - + ClauseId start_id = res->getStart(); // WHY DID WE NEED THIS? // if(isInputClause(start_id)) { - // d_seenInput.insert(start_id); + // d_seenInput.insert(start_id); // } out << clauseName(start_id) << " "; - + for(unsigned i = 0; i < steps.size(); i++) { - out << clauseName(steps[i].id) << " "<<ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")"; + out << clauseName(steps[i].id) << " "<<ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")"; } - + if (id == d_emptyClauseId) { out <<"(\\empty empty)"; - return; + return; } out << "(\\" << clauseName(id) << "\n"; // bind to lemma name diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index a4178f518..d555ca529 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -9,7 +9,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Resolution proof + ** \brief Resolution proof ** ** Resolution proof **/ @@ -43,11 +43,11 @@ namespace std { namespace CVC4 { -/** +/** * Helper debugging functions */ void printDebug(::Minisat::Lit l); -void printDebug(::Minisat::Clause& c); +void printDebug(::Minisat::Clause& c); struct ResStep { ::Minisat::Lit lit; @@ -60,8 +60,8 @@ struct ResStep { {} };/* struct ResStep */ -typedef std::vector< ResStep > ResSteps; -typedef std::set < ::Minisat::Lit> LitSet; +typedef std::vector< ResStep > ResSteps; +typedef std::set < ::Minisat::Lit> LitSet; class ResChain { private: @@ -72,7 +72,7 @@ public: ResChain(ClauseId start); void addStep(::Minisat::Lit, ClauseId, bool); bool redundantRemoved() { return (d_redundantLits == NULL || d_redundantLits->empty()); } - void addRedundantLit(::Minisat::Lit lit); + void addRedundantLit(::Minisat::Lit lit); ~ResChain(); // accessor methods ClauseId getStart() { return d_start; } @@ -83,16 +83,16 @@ public: typedef std::hash_map < ClauseId, ::Minisat::CRef > IdCRefMap; typedef std::hash_map < ::Minisat::CRef, ClauseId > ClauseIdMap; typedef std::hash_map < ClauseId, ::Minisat::Lit> IdUnitMap; -typedef std::hash_map < int, ClauseId> UnitIdMap; //FIXME -typedef std::hash_map < ClauseId, ResChain*> IdResMap; +typedef std::hash_map < int, ClauseId> UnitIdMap; //FIXME +typedef std::hash_map < ClauseId, ResChain*> IdResMap; typedef std::hash_set < ClauseId > IdHashSet; -typedef std::vector < ResChain* > ResStack; -typedef std::hash_map <ClauseId, prop::SatClause* > IdToSatClause; -typedef std::set < ClauseId > IdSet; -typedef std::vector < ::Minisat::Lit > LitVector; +typedef std::vector < ResChain* > ResStack; +typedef std::hash_map <ClauseId, prop::SatClause* > IdToSatClause; +typedef std::set < ClauseId > IdSet; +typedef std::vector < ::Minisat::Lit > LitVector; typedef __gnu_cxx::hash_map<ClauseId, ::Minisat::Clause& > IdToMinisatClause; -class SatProof; +class SatProof; class ProofProxy : public ProofProxyAbstract { private: @@ -103,31 +103,31 @@ public: };/* class ProofProxy */ -class CnfProof; +class CnfProof; class SatProof { protected: ::Minisat::Solver* d_solver; - // clauses + // clauses IdCRefMap d_idClause; ClauseIdMap d_clauseId; IdUnitMap d_idUnit; UnitIdMap d_unitId; IdHashSet d_deleted; - IdToSatClause d_deletedTheoryLemmas; - IdHashSet d_inputClauses; - IdHashSet d_lemmaClauses; - // resolutions + IdToSatClause d_deletedTheoryLemmas; + IdHashSet d_inputClauses; + IdHashSet d_lemmaClauses; + // resolutions IdResMap d_resChains; - ResStack d_resStack; + ResStack d_resStack; bool d_checkRes; - - static ClauseId d_idCounter; + + static ClauseId d_idCounter; const ClauseId d_emptyClauseId; const ClauseId d_nullId; - // proxy class to break circular dependencies + // proxy class to break circular dependencies ProofProxy* d_proxy; - + // temporary map for updating CRefs ClauseIdMap d_temp_clauseId; IdCRefMap d_temp_idClause; @@ -135,43 +135,43 @@ protected: // unit conflict ClauseId d_unitConflictId; bool d_storedUnitConflict; -public: +public: SatProof(::Minisat::Solver* solver, bool checkRes = false); virtual ~SatProof() {} protected: - void print(ClauseId id); + void print(ClauseId id); void printRes(ClauseId id); - void printRes(ResChain* res); - + void printRes(ResChain* res); + bool isInputClause(ClauseId id); bool isLemmaClause(ClauseId id); bool isUnit(ClauseId id); - bool isUnit(::Minisat::Lit lit); - bool hasResolution(ClauseId id); - void createLitSet(ClauseId id, LitSet& set); + bool isUnit(::Minisat::Lit lit); + bool hasResolution(ClauseId id); + void createLitSet(ClauseId id, LitSet& set); void registerResolution(ClauseId id, ResChain* res); - + ClauseId getClauseId(::Minisat::CRef clause); - ClauseId getClauseId(::Minisat::Lit lit); + ClauseId getClauseId(::Minisat::Lit lit); ::Minisat::CRef getClauseRef(ClauseId id); ::Minisat::Lit getUnit(ClauseId id); - ClauseId getUnitId(::Minisat::Lit lit); + ClauseId getUnitId(::Minisat::Lit lit); ::Minisat::Clause& getClause(::Minisat::CRef ref); virtual void toStream(std::ostream& out); bool checkResolution(ClauseId id); - /** + /** * Constructs a resolution tree that proves lit * and returns the ClauseId for the unit clause lit * @param lit the literal we are proving - * - * @return + * + * @return */ ClauseId resolveUnit(::Minisat::Lit lit); - /** + /** * Does a depth first search on removed literals and adds the literals - * to be removed in the proper order to the stack. - * + * to be removed in the proper order to the stack. + * * @param lit the literal we are recursing on * @param removedSet the previously computed set of redundant literals * @param removeStack the stack of literals in reverse order of resolution @@ -181,71 +181,71 @@ protected: public: void startResChain(::Minisat::CRef start); void addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign); - /** + /** * Pops the current resolution of the stack and stores it * in the resolution map. Also registers the 'clause' parameter - * @param clause the clause the resolution is proving + * @param clause the clause the resolution is proving */ void endResChain(::Minisat::CRef clause); void endResChain(::Minisat::Lit lit); - /** - * Stores in the current derivation the redundant literals that were - * eliminated from the conflict clause during conflict clause minimization. - * @param lit the eliminated literal + /** + * Stores in the current derivation the redundant literals that were + * eliminated from the conflict clause during conflict clause minimization. + * @param lit the eliminated literal */ void storeLitRedundant(::Minisat::Lit lit); /// update the CRef Id maps when Minisat does memory reallocation x void updateCRef(::Minisat::CRef old_ref, ::Minisat::CRef new_ref); void finishUpdateCRef(); - - /** + + /** * Constructs the empty clause resolution from the final conflict - * - * @param conflict + * + * @param conflict */ void finalizeProof(::Minisat::CRef conflict); - /// clause registration methods + /// clause registration methods ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind = LEARNT); ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind = LEARNT); - void storeUnitConflict(::Minisat::Lit lit); - - /** + void storeUnitConflict(::Minisat::Lit lit, ClauseKind kind = LEARNT); + + /** * Marks the deleted clauses as deleted. Note we may still use them in the final - * resolution. - * @param clause + * resolution. + * @param clause */ void markDeleted(::Minisat::CRef clause); bool isDeleted(ClauseId id) { return d_deleted.find(id) != d_deleted.end(); } - /** + /** * Constructs the resolution of ~q and resolves it with the current * resolution thus eliminating q from the current clause * @param q the literal to be resolved out */ void resolveOutUnit(::Minisat::Lit q); - /** + /** * Constructs the resolution of the literal lit. Called when a clause - * containing lit becomes satisfied and is removed. - * @param lit + * containing lit becomes satisfied and is removed. + * @param lit */ - void storeUnitResolution(::Minisat::Lit lit); - + void storeUnitResolution(::Minisat::Lit lit); + ProofProxy* getProxy() {return d_proxy; } /** - Constructs the SAT proof identifying the needed lemmas + Constructs the SAT proof identifying the needed lemmas */ void constructProof(); - + protected: IdSet d_seenLearnt; IdHashSet d_seenInput; - IdHashSet d_seenLemmas; - + IdHashSet d_seenLemmas; + inline std::string varName(::Minisat::Lit lit); - inline std::string clauseName(ClauseId id); + inline std::string clauseName(ClauseId id); void collectClauses(ClauseId id); void addToProofManager(ClauseId id, ClauseKind kind); @@ -253,7 +253,7 @@ public: virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0; };/* class SatProof */ -class LFSCSatProof: public SatProof { +class LFSCSatProof : public SatProof { private: void printResolution(ClauseId id, std::ostream& out, std::ostream& paren); public: diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 696bd8309..4ed00aaaa 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -26,9 +26,10 @@ TheoryProof::TheoryProof() {} void TheoryProof::addDeclaration(Expr term) { - if (d_declarationCache.count(term)) + if (d_declarationCache.count(term)) { return; - + } + Type type = term.getType(); if (type.isSort()) d_sortDeclarations.insert(type); @@ -36,32 +37,14 @@ void TheoryProof::addDeclaration(Expr term) { Expr function = term.getOperator(); d_termDeclarations.insert(function); } else if (term.isVariable()) { - Assert (type.isSort()); + //Assert (type.isSort() || type.isBoolean()); d_termDeclarations.insert(term); } // recursively declare all other terms for (unsigned i = 0; i < term.getNumChildren(); ++i) { - addDeclaration(term[i]); - } - d_declarationCache.insert(term); -} - -void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) { - if (term.isVariable()) { - os << term; - return; - } - - Assert (term.getKind() == kind::APPLY_UF); - Expr func = term.getOperator(); - for (unsigned i = 0; i < term.getNumChildren(); ++i) { - os<< "(apply _ _ "; - } - os << func << " "; - for (unsigned i = 0; i < term.getNumChildren(); ++i) { - printTerm(term[i], os); - os << ")"; + addDeclaration(term[i]); } + d_declarationCache.insert(term); } std::string toLFSCKind(Kind kind) { @@ -70,71 +53,138 @@ std::string toLFSCKind(Kind kind) { case kind::AND: return "and"; case kind::XOR: return "xor"; case kind::EQUAL: return "="; + case kind::IFF: return "iff"; case kind::IMPLIES: return "impl"; case kind::NOT: return "not"; default: - Unreachable(); + Unreachable(); } } -void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) { - // should make this more general and overall sane - Assert (atom.getType().isBoolean() && "Only printing booleans." ); - Kind kind = atom.getKind(); - // this is the only predicate we have - if (kind == kind::EQUAL) { - os << "("; - os <<"= "; - os << atom[0].getType() <<" "; - printTerm(atom[0], os); - os <<" "; - printTerm(atom[1], os); - os <<")"; - } else if ( kind == kind::DISTINCT) { - os <<"(not (= "; - os << atom[0].getType() <<" "; - printTerm(atom[0], os); - os <<" "; - printTerm(atom[1], os); - os <<"))"; - } else if ( kind == kind::OR || - kind == kind::AND || - kind == kind::XOR || - kind == kind::IMPLIES || - kind == kind::NOT) { - // print the boolean operators +void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) { + if (term.isVariable()) { + if(term.getType().isBoolean()) { + os << "(p_app " << term << ")"; + } else { + os << term; + } + return; + } + + switch(Kind k = term.getKind()) { + case kind::APPLY_UF: { + if(term.getType().isBoolean()) { + os << "(p_app "; + } + Expr func = term.getOperator(); + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + os << "(apply _ _ "; + } + os << func << " "; + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + printTerm(term[i], os); + os << ")"; + } + if(term.getType().isBoolean()) { + os << ")"; + } + return; + } + + case kind::ITE: + os << (term.getType().isBoolean() ? "(ifte " : "(ite _ "); + printTerm(term[0], os); + os << " "; + printTerm(term[1], os); + os << " "; + printTerm(term[2], os); + os << ")"; + return; + + case kind::EQUAL: os << "("; - os << toLFSCKind(kind); - if (atom.getNumChildren() > 2) { + os << "= "; + os << term[0].getType() << " "; + printTerm(term[0], os); + os << " "; + printTerm(term[1], os); + os << ")"; + return; + + case kind::DISTINCT: + os << "(not (= "; + os << term[0].getType() << " "; + printTerm(term[0], os); + os << " "; + printTerm(term[1], os); + os << "))"; + return; + + case kind::OR: + case kind::AND: + case kind::XOR: + case kind::IFF: + case kind::IMPLIES: + case kind::NOT: + // print the Boolean operators + os << "(" << toLFSCKind(k); + if(term.getNumChildren() > 2) { + // LFSC doesn't allow declarations with variable numbers of + // arguments, so we have to flatten these N-ary versions. std::ostringstream paren; os << " "; - for (unsigned i =0; i < atom.getNumChildren(); ++i) { - printFormula(atom[i], os); + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + printTerm(term[i], os); os << " "; - if (i < atom.getNumChildren() - 2) { - os << "("<< toLFSCKind(kind) << " "; - paren << ")"; + if(i < term.getNumChildren() - 2) { + os << "(" << toLFSCKind(k) << " "; + paren << ")"; } } - os << paren.str() <<")"; + os << paren.str() << ")"; } else { - // this is for binary and unary operators - for (unsigned i = 0; i < atom.getNumChildren(); ++i) { - os <<" "; - printFormula(atom[i], os); + // this is for binary and unary operators + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + os << " "; + printTerm(term[i], os); + } + os << ")"; + } + return; + + case kind::CONST_BOOLEAN: + os << (term.getConst<bool>() ? "true" : "false"); + return; + + case kind::CHAIN: { + // LFSC doesn't allow declarations with variable numbers of + // arguments, so we have to flatten chained operators, like =. + Kind op = term.getOperator().getConst<Chain>().getOperator(); + size_t n = term.getNumChildren(); + std::ostringstream paren; + for(size_t i = 1; i < n; ++i) { + if(i + 1 < n) { + os << "(" << toLFSCKind(kind::AND) << " "; + paren << ")"; + } + os << "(" << toLFSCKind(op) << " "; + printTerm(term[i - 1], os); + os << " "; + printTerm(term[i], os); + os << ")"; + if(i + 1 < n) { + os << " "; } - os <<")"; } - } else if (kind == kind::CONST_BOOLEAN) { - if (atom.getConst<bool>()) - os << "true"; - else - os << "false"; + os << paren.str(); + return; } - else { - std::cout << kind << "\n"; - Assert (false && "Unsupported kind"); + + default: + Unhandled(k); } + + Unreachable(); } void LFSCTheoryProof::printAssertions(std::ostream& os, std::ostream& paren) { @@ -142,56 +192,57 @@ void LFSCTheoryProof::printAssertions(std::ostream& os, std::ostream& paren) { ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); - // collect declarations first + // collect declarations first for(; it != end; ++it) { - addDeclaration(*it); + addDeclaration(*it); } printDeclarations(os, paren); it = ProofManager::currentPM()->begin_assertions(); for (; it != end; ++it) { os << "(% A" << counter++ << " (th_holds "; - printFormula(*it, os); + printTerm(*it, os); os << ")\n"; - paren <<")"; + paren << ")"; } } void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) { // declaring the sorts for (SortSet::const_iterator it = d_sortDeclarations.begin(); it != d_sortDeclarations.end(); ++it) { - os << "(% " << *it << " sort \n"; - paren << ")"; + os << "(% " << *it << " sort\n"; + paren << ")"; } // declaring the terms for (ExprSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) { Expr term = *it; - os << "(% " << term << " (term "; - paren <<")"; + os << "(% " << term << " "; + os << "(term "; Type type = term.getType(); if (type.isFunction()) { - std::ostringstream fparen; + std::ostringstream fparen; FunctionType ftype = (FunctionType)type; std::vector<Type> args = ftype.getArgTypes(); - args.push_back(ftype.getRangeType()); - os << "(arrow "; + args.push_back(ftype.getRangeType()); + os << "(arrow"; for (unsigned i = 0; i < args.size(); i++) { Type arg_type = args[i]; - Assert (arg_type.isSort()); - os << arg_type << " "; + //Assert (arg_type.isSort() || arg_type.isBoolean()); + os << " " << arg_type; if (i < args.size() - 2) { - os << "(arrow "; - fparen <<")"; + os << " (arrow"; + fparen << ")"; } } - os << fparen.str() << "))\n"; + os << fparen.str() << "))\n"; } else { Assert (term.isVariable()); - Assert (type.isSort()); + //Assert (type.isSort() || type.isBoolean()); os << type << ")\n"; } + paren << ")"; } -} +} diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 457023a59..0a7772a4b 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -13,7 +13,7 @@ ** ** A manager for UfProofs. ** - ** + ** **/ @@ -24,33 +24,32 @@ #include "util/proof.h" #include "expr/expr.h" #include <ext/hash_set> -#include <iostream> +#include <iostream> namespace CVC4 { - typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet; - typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; + typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet; + typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; class TheoryProof { protected: ExprSet d_termDeclarations; - SortSet d_sortDeclarations; + SortSet d_sortDeclarations; ExprSet d_declarationCache; - - void addDeclaration(Expr atom); + public: TheoryProof(); virtual ~TheoryProof() {} virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0; + void addDeclaration(Expr atom); }; - class LFSCTheoryProof: public TheoryProof { - static void printTerm(Expr term, std::ostream& os); + class LFSCTheoryProof : public TheoryProof { void printDeclarations(std::ostream& os, std::ostream& paren); public: - static void printFormula(Expr atom, std::ostream& os); + static void printTerm(Expr term, std::ostream& os); virtual void printAssertions(std::ostream& os, std::ostream& paren); - }; + }; } /* CVC4 namespace */ #endif /* __CVC4__THEORY_PROOF_H */ diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 16fa3ba60..610023b70 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -263,7 +263,7 @@ CRef Solver::reason(Var x) { // Construct the reason CRef real_reason = ca.alloc(explLevel, explanation, true); - PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); ); + PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); ); vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x)); clauses_removable.push(real_reason); attachClause(real_reason); @@ -324,7 +324,18 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) } else { // If all false, we're in conflict if (ps.size() == falseLiteralsCount) { + if(PROOF_ON()) { + // Take care of false units here; otherwise, we need to + // construct the clause below to give to the proof manager + // as the final conflict. + if(falseLiteralsCount == 1) { + PROOF( ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT); ) + PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); ) + return ok = false; + } + } else { return ok = false; + } } CRef cr = CRef_Undef; @@ -339,7 +350,13 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) clauses_persistent.push(cr); attachClause(cr); - PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT); ) + if(PROOF_ON()) { + PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT); ) + if(ps.size() == falseLiteralsCount) { + PROOF( ProofManager::getSatProof()->finalizeProof(cr); ) + return ok = false; + } + } } // Check if it propagates @@ -347,8 +364,17 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) if(assigns[var(ps[0])] == l_Undef) { assert(assigns[var(ps[0])] != l_False); uncheckedEnqueue(ps[0], cr); - PROOF( if (ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); } ) - return ok = (propagate(CHECK_WITHOUT_THEORY) == CRef_Undef); + PROOF( if(ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); } ); + CRef confl = propagate(CHECK_WITHOUT_THEORY); + if(! (ok = (confl == CRef_Undef)) ) { + if(ca[confl].size() == 1) { + PROOF( ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT); ); + PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); ) + } else { + PROOF( ProofManager::getSatProof()->finalizeProof(confl); ); + } + } + return ok; } else return ok; } } @@ -370,7 +396,7 @@ void Solver::attachClause(CRef cr) { void Solver::detachClause(CRef cr, bool strict) { const Clause& c = ca[cr]; - PROOF( ProofManager::getSatProof()->markDeleted(cr); ) + PROOF( ProofManager::getSatProof()->markDeleted(cr); ); Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl; assert(c.size() > 1); @@ -1580,7 +1606,7 @@ CRef Solver::updateLemmas() { vec<Lit>& lemma = lemmas[i]; // If it's an empty lemma, we have a conflict at zero level if (lemma.size() == 0) { - Assert (! PROOF_ON()); + Assert (! PROOF_ON()); conflict = CRef_Lazy; backtrackLevel = 0; Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl; @@ -1630,13 +1656,15 @@ CRef Solver::updateLemmas() { } lemma_ref = ca.alloc(clauseLevel, lemma, removable); - PROOF (ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); ); + PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); ); if (removable) { clauses_removable.push(lemma_ref); } else { clauses_persistent.push(lemma_ref); } attachClause(lemma_ref); + } else { + PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); ); } // If the lemma is propagating enqueue its literal (or set the conflict) @@ -1650,7 +1678,7 @@ CRef Solver::updateLemmas() { } else { Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl; conflict = CRef_Lazy; - PROOF(ProofManager::getSatProof()->storeUnitConflict(lemma[0]);); + PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0]); ); } } else { Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl; diff --git a/src/smt/options b/src/smt/options index 05a138f60..b76822caf 100644 --- a/src/smt/options +++ b/src/smt/options @@ -22,12 +22,16 @@ option expandDefinitions expand-definitions bool :default false always expand symbol definitions in output common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h" support the get-value and get-model commands -option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" +option checkModels check-models --check-models bool :link --produce-models --interactive :link-smt produce-models :link-smt interactive-mode :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions -option dumpModels --dump-models bool :default false +option dumpModels --dump-models bool :default false :link --produce-models output models after every SAT/INVALID/UNKNOWN response option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on proof generation +option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" + after UNSAT/VALID, machine-check the generated proof +option dumpProofs --dump-proofs bool :default false :link --proof + output proofs after every UNSAT/VALID response # this is just a placeholder for later; it doesn't show up in command-line options listings undocumented-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on unsat core generation (NOT YET SUPPORTED) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0fadca424..f26456cae 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -46,8 +46,10 @@ #include "theory/theory_engine.h" #include "theory/bv/theory_bv_rewriter.h" #include "proof/proof_manager.h" +#include "main/options.h" #include "util/proof.h" #include "proof/proof.h" +#include "proof/proof_manager.h" #include "util/boolean_simplification.h" #include "util/node_visitor.h" #include "util/configuration.h" @@ -157,6 +159,8 @@ struct SmtEngineStatistics { IntStat d_numAssertionsPost; /** time spent in checkModel() */ TimerStat d_checkModelTime; + /** time spent in checkProof() */ + TimerStat d_checkProofTime; /** time spent in PropEngine::checkSat() */ TimerStat d_solveTime; /** time spent in pushing/popping */ @@ -183,11 +187,11 @@ struct SmtEngineStatistics { d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0), d_checkModelTime("smt::SmtEngine::checkModelTime"), + d_checkProofTime("smt::SmtEngine::checkProofTime"), d_solveTime("smt::SmtEngine::solveTime"), d_pushPopTime("smt::SmtEngine::pushPopTime"), d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"), d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0) - { StatisticsRegistry::registerStat(&d_definitionExpansionTime); @@ -667,6 +671,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_decisionEngine(NULL), d_theoryEngine(NULL), d_propEngine(NULL), + d_proofManager(NULL), d_definedFunctions(NULL), d_assertionList(NULL), d_assignments(NULL), @@ -696,6 +701,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_statisticsRegistry = new StatisticsRegistry(); d_stats = new SmtEngineStatistics(); + PROOF( d_proofManager = new ProofManager(); ); + // 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, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic)); @@ -763,6 +770,7 @@ void SmtEngine::finishInit() { if(options::cumulativeMillisecondLimit() != 0) { setTimeLimit(options::cumulativeMillisecondLimit(), true); } + PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); ); } @@ -777,16 +785,11 @@ void SmtEngine::finalOptionsAreSet() { } if(options::checkModels()) { - if(! options::produceModels()) { - Notice() << "SmtEngine: turning on produce-models to support check-model" << endl; - setOption("produce-models", SExpr("true")); - } if(! options::interactive()) { - Notice() << "SmtEngine: turning on interactive-mode to support check-model" << endl; + Notice() << "SmtEngine: turning on interactive-mode to support check-models" << endl; setOption("interactive-mode", SExpr("true")); } } - if(options::produceAssignments() && !options::produceModels()) { Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl; setOption("produce-models", SExpr("true")); @@ -2503,7 +2506,7 @@ void SmtEnginePrivate::doMiplibTrick() { const uint64_t mark = (*j).second; const unsigned numVars = pos.getKind() == kind::AND ? pos.getNumChildren() : 1; uint64_t expected = (uint64_t(1) << (1 << numVars)) - 1; - expected = (expected == 0) ? -1 : expected;// fix for overflow + expected = (expected == 0) ? -1 : expected; // fix for overflow Debug("miplib") << "[" << pos << "] => " << hex << mark << " expect " << expected << dec << endl; Assert(pos.getKind() == kind::AND || pos.isVar()); if(mark != expected) { @@ -2511,7 +2514,7 @@ void SmtEnginePrivate::doMiplibTrick() { } else { if(mark != 3) { // exclude single-var case; nothing to check there uint64_t sz = (uint64_t(1) << checks[pos_var].size()) - 1; - sz = (sz == 0) ? -1 : sz;// fix for overflow + sz = (sz == 0) ? -1 : sz; // fix for overflow Assert(sz == mark, "expected size %u == mark %u", sz, mark); for(size_t k = 0; k < checks[pos_var].size(); ++k) { if((k & (k - 1)) != 0) { @@ -2531,12 +2534,12 @@ void SmtEnginePrivate::doMiplibTrick() { break; } } else { - Assert(checks[pos_var][k] == 0, "checks[(%s,%s)][%u] should be 0, but it's %s", pos.toString().c_str(), var.toString().c_str(), k, checks[pos_var][k].toString().c_str());// we never set for single-positive-var + Assert(checks[pos_var][k] == 0, "checks[(%s,%s)][%u] should be 0, but it's %s", pos.toString().c_str(), var.toString().c_str(), k, checks[pos_var][k].toString().c_str()); // we never set for single-positive-var } } } if(!eligible) { - eligible = true;// next is still eligible + eligible = true; // next is still eligible continue; } @@ -2560,7 +2563,7 @@ void SmtEnginePrivate::doMiplibTrick() { Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one)); d_assertionsToCheck.push_back(Rewriter::rewrite(geq.andNode(leq))); SubstitutionMap nullMap(&d_fakeContext); - Theory::PPAssertStatus status CVC4_UNUSED;// just for assertions + Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions status = d_smt.d_theoryEngine->solve(geq, nullMap); Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED, "unexpected solution from arith's ppAssert()"); @@ -3291,9 +3294,6 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc finalOptionsAreSet(); doPendingPops(); - - PROOF( ProofManager::currentPM()->addAssertion(ex); ); - Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl; if(d_queryMade && !options::incrementalSolving()) { @@ -3308,6 +3308,8 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); // Ensure expr is type-checked at this point. ensureBoolean(e); + // Give it to proof manager + PROOF( ProofManager::currentPM()->addAssertion(e); ); } // check to see if a postsolve() is pending @@ -3358,6 +3360,13 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc checkModel(/* hard failure iff */ ! r.isUnknown()); } } + // Check that UNSAT results generate a proof correctly. + if(options::checkProofs()) { + if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime); + checkProof(); + } + } return r; }/* SmtEngine::checkSat() */ @@ -3378,9 +3387,10 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept // Substitute out any abstract values in ex Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); - // Ensure that the expression is type-checked at this point, and Boolean ensureBoolean(e); + // Give it to proof manager + PROOF( ProofManager::currentPM()->addAssertion(e.notExpr()); ); // check to see if a postsolve() is pending if(d_needPostsolve) { @@ -3428,6 +3438,13 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept checkModel(/* hard failure iff */ ! r.isUnknown()); } } + // Check that UNSAT results generate a proof correctly. + if(options::checkProofs()) { + if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime); + checkProof(); + } + } return r; }/* SmtEngine::query() */ @@ -3437,7 +3454,9 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); - PROOF( ProofManager::currentPM()->addAssertion(ex);); + + PROOF( ProofManager::currentPM()->addAssertion(ex); ); + Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl; // Substitute out any abstract values in ex @@ -3474,7 +3493,7 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); if( options::typeChecking() ) { - e.getType(true);// ensure expr is type-checked at this point + e.getType(true); // ensure expr is type-checked at this point } // Make sure all preprocessing is done diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 9655297b3..8e400468c 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -56,6 +56,8 @@ class SmtEngine; class DecisionEngine; class TheoryEngine; +class ProofManager; + class Model; class StatisticsRegistry; @@ -83,6 +85,7 @@ namespace smt { class BooleanTermConverter; void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); + ProofManager* currentProofManager(); struct CommandCleanup; typedef context::CDList<Command*, CommandCleanup> CommandList; @@ -135,8 +138,11 @@ class CVC4_PUBLIC SmtEngine { TheoryEngine* d_theoryEngine; /** The propositional engine */ prop::PropEngine* d_propEngine; + /** The proof manager */ + ProofManager* d_proofManager; /** An index of our defined functions */ DefinedFunctionMap* d_definedFunctions; + /** * The assertion list (before any conversion) for supporting * getAssertions(). Only maintained if in interactive mode. @@ -249,6 +255,11 @@ class CVC4_PUBLIC SmtEngine { smt::SmtEnginePrivate* d_private; /** + * Check that a generated Proof (via getProof()) checks. + */ + void checkProof(); + + /** * Check that a generated Model (via getModel()) actually satisfies * all user assertions. */ @@ -322,6 +333,7 @@ class CVC4_PUBLIC SmtEngine { friend class ::CVC4::smt::BooleanTermConverter; friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*); friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); + friend ProofManager* ::CVC4::smt::currentProofManager(); // to access d_modelCommands friend class ::CVC4::Model; friend class ::CVC4::theory::TheoryModel; diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i index ff4105241..00c332bd1 100644 --- a/src/smt/smt_engine.i +++ b/src/smt/smt_engine.i @@ -43,8 +43,8 @@ SWIGEXPORT void JNICALL Java_edu_nyu_acsys_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jc } %ignore CVC4::SmtEngine::setLogic(const char*); -%ignore CVC4::SmtEngine::getProof; %ignore CVC4::stats::getStatisticsRegistry(SmtEngine*); %ignore CVC4::smt::beforeSearch(std::string, bool, SmtEngine*); +%ignore CVC4::smt::currentProofManager(); %include "smt/smt_engine.h" diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp new file mode 100644 index 000000000..a731ff024 --- /dev/null +++ b/src/smt/smt_engine_check_proof.cpp @@ -0,0 +1,95 @@ +/********************* */ +/*! \file smt_engine_check_proof.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "smt/smt_engine.h" +#include "util/statistics_registry.h" +#include "check.h" + +#include <cstdlib> +#include <cstring> +#include <fstream> +#include <string> +#include <unistd.h> + +using namespace CVC4; +using namespace std; + +namespace CVC4 { + +namespace proof { + extern const char *const plf_signatures; +}/* CVC4::proof namespace */ + +namespace smt { + +class UnlinkProofFile { + string d_filename; +public: + UnlinkProofFile(const char* filename) : d_filename(filename) {} + ~UnlinkProofFile() { unlink(d_filename.c_str()); } +};/* class UnlinkProofFile */ + +}/* CVC4::smt namespace */ + +}/* CVC4 namespace */ + +void SmtEngine::checkProof() { + +#ifdef CVC4_PROOF + + Chat() << "generating proof..." << endl; + + Proof* pf = getProof(); + + Chat() << "checking proof..." << endl; + + if(!d_logic.isPure(theory::THEORY_BOOL) && + !d_logic.isPure(theory::THEORY_UF)) { + // no checking for these yet + Notice() << "Notice: no proof-checking for non-UF proofs yet" << endl; + return; + } + + char* pfFile = strdup("/tmp/cvc4_proof.XXXXXX"); + int fd = mkstemp(pfFile); + + // ensure this temp file is removed after + smt::UnlinkProofFile unlinker(pfFile); + + ofstream pfStream(pfFile); + pfStream << proof::plf_signatures << endl; + pf->toStream(pfStream); + pfStream.close(); + args a; + a.show_runs = false; + a.no_tail_calls = false; + a.compile_scc = false; + a.compile_scc_debug = false; + a.run_scc = false; + a.use_nested_app = false; + a.compile_lib = false; + init(); + check_file(pfFile, args()); + close(fd); + +#else /* CVC4_PROOF */ + + Unreachable("This version of CVC4 was built without proof support; cannot check proofs."); + +#endif /* CVC4_PROOF */ + +} diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index 21644d3f4..2389181b5 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -22,10 +22,14 @@ #include "util/cvc4_assert.h" #include "expr/node_manager.h" #include "util/output.h" +#include "proof/proof.h" #pragma once namespace CVC4 { + +class ProofManager; + namespace smt { extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current; @@ -35,6 +39,12 @@ inline SmtEngine* currentSmtEngine() { return s_smtEngine_current; } +inline ProofManager* currentProofManager() { + Assert(PROOF_ON()); + Assert(s_smtEngine_current != NULL); + return s_smtEngine_current->d_proofManager; +} + class SmtScope : public NodeManagerScope { /** The old NodeManager, to be restored on destruction. */ SmtEngine* d_oldSmtEngine; diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 20db916c9..a421d6fa8 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -11,12 +11,11 @@ typechecker "theory/strings/theory_strings_type_rules.h" operator STRING_CONCAT 2: "string concat" - operator STRING_IN_REGEXP 2 "membership" - operator STRING_LENGTH 1 "string length" - operator STRING_SUBSTR 3 "string substr" +operator STRING_STRCTN 2 "string contains" +operator STRING_CHARAT 2 "string char at" #sort CHAR_TYPE \ # Cardinality::INTEGERS \ @@ -104,6 +103,8 @@ typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule +typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule +typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index ff01b1887..111c4f51d 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -136,6 +136,61 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { } else { throw LogicException("substring not supported in this release"); } + } else if( t.getKind() == kind::STRING_STRCTN ){ + if(options::stringExp()) { + Node w = simplify( t[0], new_nodes ); + Node y = simplify( t[1], new_nodes ); + Node emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); + std::vector< Node > or_vec; + or_vec.push_back( w.eqNode(y) ); + Node x1 = NodeManager::currentNM()->mkBoundVar( t[0].getType() ); + Node b1 = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, x1 ); + Node c1 = NodeManager::currentNM()->mkNode( kind::EXISTS, b1, NodeManager::currentNM()->mkNode( kind::AND, + x1.eqNode( emptyString ).negate(), + w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, x1, y ) ))); + or_vec.push_back( c1 ); + Node z2 = NodeManager::currentNM()->mkBoundVar( t[0].getType() ); + Node b2 = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, z2 ); + Node c2 = NodeManager::currentNM()->mkNode( kind::EXISTS, b2, NodeManager::currentNM()->mkNode( kind::AND, + z2.eqNode( emptyString ).negate(), + w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, y, z2 ) ))); + or_vec.push_back( c2 ); + Node x3 = NodeManager::currentNM()->mkBoundVar( t[0].getType() ); + Node z3 = NodeManager::currentNM()->mkBoundVar( t[0].getType() ); + Node b3 = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, x3, z3 ); + Node c3 = NodeManager::currentNM()->mkNode( kind::EXISTS, b3, NodeManager::currentNM()->mkNode( kind::AND, + x3.eqNode( emptyString ).negate(), z3.eqNode( emptyString ).negate(), + w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, x3, y, z3 ) ))); + or_vec.push_back( c3 ); + + Node cc = NodeManager::currentNM()->mkNode( kind::OR, or_vec ); + + d_cache[t] = cc; + retNode = cc; + } else { + throw LogicException("string contain not supported in this release"); + } + } else if( t.getKind() == kind::STRING_CHARAT ){ + if(options::stringExp()) { + Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1sym_$$", t.getType(), "created for charat" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "ca2sym_$$", t.getType(), "created for charat" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3sym_$$", t.getType(), "created for charat" ); + Node x = simplify( t[0], new_nodes ); + Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x ); + new_nodes.push_back( x_eq_123 ); + Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1], + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); + new_nodes.push_back( len_sk1_eq_i ); + Node len_sk2_eq_1 = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkConst( Rational( 1 ) ), + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) ); + new_nodes.push_back( len_sk2_eq_1 ); + + d_cache[t] = sk2; + retNode = sk2; + } else { + throw LogicException("string char at not supported in this release"); + } } else if( t.getNumChildren()>0 ){ std::vector< Node > cc; if (t.getMetaKind() == kind::metakind::PARAMETERIZED) { diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 0e37367bf..af19095a0 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -341,21 +341,35 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } } } else if(node.getKind() == kind::STRING_SUBSTR) { - if(options::stringExp()) { - if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) { - int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt(); - int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); - if( node[0].getConst<String>().size() >= (unsigned) (i + j) ) { - retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) ); - } else { - // TODO: some issues, must be guarded by users - retNode = NodeManager::currentNM()->mkConst( false ); - } + if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) { + int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt(); + int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); + if( node[0].getConst<String>().size() >= (unsigned) (i + j) ) { + retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) ); } else { - //handled by preprocess + // TODO: some issues, must be guarded by users + retNode = NodeManager::currentNM()->mkConst( false ); + } + } + } else if(node.getKind() == kind::STRING_STRCTN) { + if( node[0].isConst() && node[1].isConst() ) { + CVC4::String s = node[0].getConst<String>(); + CVC4::String t = node[1].getConst<String>(); + if( s.find(t) != std::string::npos ) { + retNode = NodeManager::currentNM()->mkConst( true ); + } else { + retNode = NodeManager::currentNM()->mkConst( false ); + } + } + } else if(node.getKind() == kind::STRING_CHARAT) { + if( node[0].isConst() && node[1].isConst() ) { + int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt(); + if( node[0].getConst<String>().size() > (unsigned) i ) { + retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, 1) ); + } else { + // TODO: some issues, must be guarded by users + retNode = NodeManager::currentNM()->mkConst( false ); } - } else { - throw LogicException("substring not supported in this release"); } } else if(node.getKind() == kind::STRING_IN_REGEXP) { retNode = rewriteMembership(node); diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index d5019ab39..9d3197517 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -73,15 +73,51 @@ public: if( check ){ TypeNode t = n[0].getType(check); if (!t.isString()) { - throw TypeCheckingExceptionPrivate(n, "expecting string terms in substr"); + throw TypeCheckingExceptionPrivate(n, "expecting a string term in substr"); } t = n[1].getType(check); if (!t.isInteger()) { - throw TypeCheckingExceptionPrivate(n, "expecting start int terms in substr"); + throw TypeCheckingExceptionPrivate(n, "expecting a start int term in substr"); } t = n[2].getType(check); if (!t.isInteger()) { - throw TypeCheckingExceptionPrivate(n, "expecting length int terms in substr"); + throw TypeCheckingExceptionPrivate(n, "expecting a length int term in substr"); + } + } + return nodeManager->stringType(); + } +}; + +class StringContainTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if( check ){ + TypeNode t = n[0].getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting an orginal string term in string contain"); + } + t = n[1].getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting a target string term in string contain"); + } + } + return nodeManager->booleanType(); + } +}; + +class StringCharAtTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if( check ){ + TypeNode t = n[0].getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at"); + } + t = n[1].getType(check); + if (!t.isInteger()) { + throw TypeCheckingExceptionPrivate(n, "expecting an integer string term in string char at"); } } return nodeManager->stringType(); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 7cf4d7ad9..c598fd01b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -146,6 +146,7 @@ TheoryEngine::TheoryEngine(context::Context* context, StatisticsRegistry::registerStat(&d_combineTheoriesTime); d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); + PROOF (ProofManager::currentPM()->initTheoryProof(); ); d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor()); diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 2f278625a..1d6ce1a73 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -144,7 +144,8 @@ EXTRA_DIST = \ predicate.i \ uninterpreted_constant.i \ chain.i \ - regexp.i + regexp.i \ + proof.i DISTCLEANFILES = \ integer.h.tmp \ diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 5fa893336..8d70e4ffc 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -102,7 +102,7 @@ void Datatype::resolve(ExprManager* em, CheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!"); d_resolved = true; size_t index = 0; - for(iterator i = begin(), i_end = end(); i != i_end; ++i) { + for(std::vector<DatatypeConstructor>::iterator i = d_constructors.begin(), i_end = d_constructors.end(); i != i_end; ++i) { (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements); Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index); Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++); @@ -416,7 +416,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, NodeManager* nm = NodeManager::fromExprManager(em); TypeNode selfTypeNode = TypeNode::fromType(self); size_t index = 0; - for(iterator i = begin(), i_end = end(); i != i_end; ++i) { + for(std::vector<DatatypeConstructorArg>::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) { if((*i).d_selector.isNull()) { // the unresolved type wasn't created here; do name resolution string typeName = (*i).d_name.substr((*i).d_name.find('\0') + 1); @@ -461,7 +461,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, d_tester = nm->mkSkolem(getTesterName(), nm->mkTesterType(selfTypeNode), "is a tester", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr(); d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode), "is a constructor", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr(); // associate constructor with all selectors - for(iterator i = begin(), i_end = end(); i != i_end; ++i) { + for(std::vector<DatatypeConstructorArg>::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) { (*i).d_constructor = d_constructor; } } diff --git a/src/util/datatype.h b/src/util/datatype.h index 802704803..99a303950 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -40,6 +40,47 @@ namespace CVC4 { class CVC4_PUBLIC ExprManager; +class CVC4_PUBLIC DatatypeConstructor; +class CVC4_PUBLIC DatatypeConstructorArg; + +class CVC4_PUBLIC DatatypeConstructorIterator { + const std::vector<DatatypeConstructor>* d_v; + size_t d_i; + + friend class Datatype; + + DatatypeConstructorIterator(const std::vector<DatatypeConstructor>& v, bool start) : d_v(&v), d_i(start ? 0 : v.size()) { + } + +public: + typedef const DatatypeConstructor& value_type; + const DatatypeConstructor& operator*() const { return (*d_v)[d_i]; } + const DatatypeConstructor* operator->() const { return &(*d_v)[d_i]; } + DatatypeConstructorIterator& operator++() { ++d_i; return *this; } + DatatypeConstructorIterator operator++(int) { DatatypeConstructorIterator i(*this); ++d_i; return i; } + bool operator==(const DatatypeConstructorIterator& other) const { return d_v == other.d_v && d_i == other.d_i; } + bool operator!=(const DatatypeConstructorIterator& other) const { return d_v != other.d_v || d_i != other.d_i; } +};/* class DatatypeConstructorIterator */ + +class CVC4_PUBLIC DatatypeConstructorArgIterator { + const std::vector<DatatypeConstructorArg>* d_v; + size_t d_i; + + friend class DatatypeConstructor; + + DatatypeConstructorArgIterator(const std::vector<DatatypeConstructorArg>& v, bool start) : d_v(&v), d_i(start ? 0 : v.size()) { + } + +public: + typedef const DatatypeConstructorArg& value_type; + const DatatypeConstructorArg& operator*() const { return (*d_v)[d_i]; } + const DatatypeConstructorArg* operator->() const { return &(*d_v)[d_i]; } + DatatypeConstructorArgIterator& operator++() { ++d_i; return *this; } + DatatypeConstructorArgIterator operator++(int) { DatatypeConstructorArgIterator i(*this); ++d_i; return i; } + bool operator==(const DatatypeConstructorArgIterator& other) const { return d_v == other.d_v && d_i == other.d_i; } + bool operator!=(const DatatypeConstructorArgIterator& other) const { return d_v != other.d_v || d_i != other.d_i; } +};/* class DatatypeConstructorArgIterator */ + /** * An exception that is thrown when a datatype resolution fails. */ @@ -134,9 +175,9 @@ class CVC4_PUBLIC DatatypeConstructor { public: /** The type for iterators over constructor arguments. */ - typedef std::vector<DatatypeConstructorArg>::iterator iterator; + typedef DatatypeConstructorArgIterator iterator; /** The (const) type for iterators over constructor arguments. */ - typedef std::vector<DatatypeConstructorArg>::const_iterator const_iterator; + typedef DatatypeConstructorArgIterator const_iterator; private: @@ -394,9 +435,9 @@ public: static size_t indexOf(Expr item) CVC4_PUBLIC; /** The type for iterators over constructors. */ - typedef std::vector<DatatypeConstructor>::iterator iterator; + typedef DatatypeConstructorIterator iterator; /** The (const) type for iterators over constructors. */ - typedef std::vector<DatatypeConstructor>::const_iterator const_iterator; + typedef DatatypeConstructorIterator const_iterator; private: std::string d_name; @@ -540,13 +581,13 @@ public: inline bool isResolved() const throw(); /** Get the beginning iterator over DatatypeConstructors. */ - inline std::vector<DatatypeConstructor>::iterator begin() throw(); + inline iterator begin() throw(); /** Get the ending iterator over DatatypeConstructors. */ - inline std::vector<DatatypeConstructor>::iterator end() throw(); + inline iterator end() throw(); /** Get the beginning const_iterator over DatatypeConstructors. */ - inline std::vector<DatatypeConstructor>::const_iterator begin() const throw(); + inline const_iterator begin() const throw(); /** Get the ending const_iterator over DatatypeConstructors. */ - inline std::vector<DatatypeConstructor>::const_iterator end() const throw(); + inline const_iterator end() const throw(); /** Get the ith DatatypeConstructor. */ const DatatypeConstructor& operator[](size_t index) const; @@ -669,19 +710,19 @@ inline bool Datatype::isResolved() const throw() { } inline Datatype::iterator Datatype::begin() throw() { - return d_constructors.begin(); + return iterator(d_constructors, true); } inline Datatype::iterator Datatype::end() throw() { - return d_constructors.end(); + return iterator(d_constructors, false); } inline Datatype::const_iterator Datatype::begin() const throw() { - return d_constructors.begin(); + return const_iterator(d_constructors, true); } inline Datatype::const_iterator Datatype::end() const throw() { - return d_constructors.end(); + return const_iterator(d_constructors, false); } inline bool DatatypeConstructor::isResolved() const throw() { @@ -710,19 +751,19 @@ inline bool DatatypeConstructorArg::isResolved() const throw() { } inline DatatypeConstructor::iterator DatatypeConstructor::begin() throw() { - return d_args.begin(); + return iterator(d_args, true); } inline DatatypeConstructor::iterator DatatypeConstructor::end() throw() { - return d_args.end(); + return iterator(d_args, false); } inline DatatypeConstructor::const_iterator DatatypeConstructor::begin() const throw() { - return d_args.begin(); + return const_iterator(d_args, true); } inline DatatypeConstructor::const_iterator DatatypeConstructor::end() const throw() { - return d_args.end(); + return const_iterator(d_args, false); } }/* CVC4 namespace */ diff --git a/src/util/datatype.i b/src/util/datatype.i index c07caa805..403fb31bc 100644 --- a/src/util/datatype.i +++ b/src/util/datatype.i @@ -1,5 +1,12 @@ %{ #include "util/datatype.h" + +#ifdef SWIGJAVA + +#include "bindings/java_iterator_adapter.h" +#include "bindings/java_stream_adapters.h" + +#endif /* SWIGJAVA */ %} %extend std::vector< CVC4::Datatype > { @@ -32,34 +39,137 @@ %ignore set(int i, const CVC4::Datatype::Constructor& x); %ignore to_array(); }; -%template(vectorDatatypeConstructor) std::vector< CVC4::DatatypeConstructor >; +//%template(vectorDatatypeConstructor) std::vector< CVC4::DatatypeConstructor >; %rename(equals) CVC4::Datatype::operator==(const Datatype&) const; %ignore CVC4::Datatype::operator!=(const Datatype&) const; -%rename(beginConst) CVC4::Datatype::begin() const; -%rename(endConst) CVC4::Datatype::end() const; +%ignore CVC4::Datatype::begin(); +%ignore CVC4::Datatype::end(); +%ignore CVC4::Datatype::begin() const; +%ignore CVC4::Datatype::end() const; -%rename(getConstructor) CVC4::Datatype::operator[](size_t) const; -%ignore CVC4::Datatype::operator[](std::string) const; +%rename(get) CVC4::Datatype::operator[](size_t) const; +%rename(get) CVC4::Datatype::operator[](std::string) const; %rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const; %ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const; %rename(apply) CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor&) const; %ignore CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor*) const; -%rename(beginConst) CVC4::DatatypeConstructor::begin() const; -%rename(endConst) CVC4::DatatypeConstructor::end() const; +%ignore CVC4::DatatypeConstructor::begin(); +%ignore CVC4::DatatypeConstructor::end(); +%ignore CVC4::DatatypeConstructor::begin() const; +%ignore CVC4::DatatypeConstructor::end() const; -%rename(getArg) CVC4::DatatypeConstructor::operator[](size_t) const; -%rename(getArg) CVC4::DatatypeConstructor::operator[](std::string) const; +%rename(get) CVC4::DatatypeConstructor::operator[](size_t) const; +%rename(get) CVC4::DatatypeConstructor::operator[](std::string) const; %ignore CVC4::operator<<(std::ostream&, const Datatype&); %ignore CVC4::operator<<(std::ostream&, const DatatypeConstructor&); %ignore CVC4::operator<<(std::ostream&, const DatatypeConstructorArg&); +%ignore CVC4::DatatypeConstructorIterator; +%ignore CVC4::DatatypeConstructorArgIterator; + %feature("valuewrapper") CVC4::DatatypeUnresolvedType; %feature("valuewrapper") CVC4::DatatypeConstructor; +#ifdef SWIGJAVA + +// Instead of Datatype::begin() and end(), create an +// iterator() method on the Java side that returns a Java-style +// Iterator. +%extend CVC4::Datatype { + CVC4::JavaIteratorAdapter<CVC4::Datatype> iterator() { + return CVC4::JavaIteratorAdapter<CVC4::Datatype>(*$self); + } + + std::string toString() const { + std::stringstream ss; + ss << *$self; + return ss.str(); + } +} +%extend CVC4::DatatypeConstructor { + CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> iterator() { + return CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor>(*$self); + } + + std::string toString() const { + std::stringstream ss; + ss << *$self; + return ss.str(); + } +} +%extend CVC4::DatatypeConstructorArg { + std::string toString() const { + std::stringstream ss; + ss << *$self; + return ss.str(); + } +} + +// Datatype is "iterable" on the Java side +%typemap(javainterfaces) CVC4::Datatype "java.lang.Iterable<DatatypeConstructor>"; +%typemap(javainterfaces) CVC4::DatatypeConstructor "java.lang.Iterable<DatatypeConstructorArg>"; + +// the JavaIteratorAdapter should not be public, and implements Iterator +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Datatype> "class"; +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Datatype> "java.util.Iterator<DatatypeConstructor>"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> "java.util.Iterator<DatatypeConstructorArg>"; +// add some functions to the Java side (do it here because there's no way to do these in C++) +%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::Datatype> " + public void remove() { + throw new java.lang.UnsupportedOperationException(); + } + + public DatatypeConstructor next() { + if(hasNext()) { + return getNext(); + } else { + throw new java.util.NoSuchElementException(); + } + } +" +%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> " + public void remove() { + throw new java.lang.UnsupportedOperationException(); + } + + public DatatypeConstructorArg next() { + if(hasNext()) { + return getNext(); + } else { + throw new java.util.NoSuchElementException(); + } + } +" +// getNext() just allows C++ iterator access from Java-side next(), make it private +%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Datatype>::getNext() "private"; +%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor>::getNext() "private"; + +// map the types appropriately. +%typemap(jni) CVC4::Datatype::iterator::value_type "jobject"; +%typemap(jtype) CVC4::Datatype::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructor"; +%typemap(jstype) CVC4::Datatype::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructor"; +%typemap(javaout) CVC4::Datatype::iterator::value_type { return $jnicall; } +%typemap(jni) CVC4::DatatypeConstructor::iterator::value_type "jobject"; +%typemap(jtype) CVC4::DatatypeConstructor::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructorArg"; +%typemap(jstype) CVC4::DatatypeConstructor::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructorArg"; +%typemap(javaout) CVC4::DatatypeConstructor::iterator::value_type { return $jnicall; } + +#endif /* SWIGJAVA */ + %include "util/datatype.h" +#ifdef SWIGJAVA + +%include "bindings/java_iterator_adapter.h" +%include "bindings/java_stream_adapters.h" + +%template(JavaIteratorAdapter_Datatype) CVC4::JavaIteratorAdapter<CVC4::Datatype>; +%template(JavaIteratorAdapter_DatatypeConstructor) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor>; + +#endif /* SWIGJAVA */ diff --git a/src/util/proof.i b/src/util/proof.i new file mode 100644 index 000000000..22dff1043 --- /dev/null +++ b/src/util/proof.i @@ -0,0 +1,5 @@ +%{ +#include "util/proof.h" +%} + +%include "util/proof.h" diff --git a/src/util/regexp.h b/src/util/regexp.h index 3a8fc7170..3f9df6aaf 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -183,6 +183,25 @@ public: return true; } + std::size_t find(const String &y) const { + if(y.d_str.size() == 0) return 0; + if(d_str.size() == 0) return std::string::npos; + std::size_t ret = std::string::npos; + for(int i = 0; i <= (int) d_str.size() - (int) y.d_str.size(); i++) { + if(d_str[i] == y.d_str[0]) { + std::size_t j=0; + for(; j<y.d_str.size(); j++) { + if(d_str[i+j] != y.d_str[j]) break; + } + if(j == y.d_str.size()) { + ret = (std::size_t) i; + break; + } + } + } + return ret; + } + String substr(unsigned i) const { std::vector<unsigned int> ret_vec; std::vector<unsigned int>::const_iterator itr = d_str.begin() + i; |