This command will eventually take a mode; for now it assumes a default implementation. I've opened cvc5/cvc5-wishues#104 to track this.
This is a feature requested by Certora.
return res;
}
+std::vector<Term> Term::nodeVectorToTerms(const Solver* slv,
+ const std::vector<Node>& nodes)
+{
+ std::vector<Term> res;
+ for (const Node& n : nodes)
+ {
+ res.push_back(Term(slv, n));
+ }
+ return res;
+}
+
bool Term::isReal32Value() const
{
CVC5_API_TRY_CATCH_BEGIN;
/* Can not use
* return std::vector<Term>(assertions.begin(), assertions.end());
* here since constructor is private */
- std::vector<Term> res;
- for (const Node& e : assertions)
- {
- res.push_back(Term(this, e));
- }
- return res;
+ return Term::nodeVectorToTerms(this, assertions);
////////
CVC5_API_TRY_CATCH_END;
}
CVC5_API_TRY_CATCH_END;
}
+std::vector<Term> Solver::getLearnedLiterals(void) const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK(d_slv->getOptions().smt.produceLearnedLiterals)
+ << "Cannot get learned literals unless enabled (try "
+ "--produce-learned-literals)";
+ CVC5_API_RECOVERABLE_CHECK(d_slv->getSmtMode() == SmtMode::UNSAT
+ || d_slv->getSmtMode() == SmtMode::SAT
+ || d_slv->getSmtMode() == SmtMode::SAT_UNKNOWN)
+ << "Cannot get learned literals unless after a UNSAT, SAT or UNKNOWN "
+ "response.";
+ //////// all checks before this line
+ std::vector<Node> lits = d_slv->getLearnedLiterals();
+ return Term::nodeVectorToTerms(this, lits);
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
Term Solver::getValue(const Term& term) const
{
CVC5_API_TRY_CATCH_BEGIN;
private:
/** Helper to convert a vector of Terms to internal Nodes. */
std::vector<Node> static termVectorToNodes(const std::vector<Term>& terms);
+ /** Helper to convert a vector of internal Nodes to Terms. */
+ std::vector<Term> static nodeVectorToTerms(const Solver* slv,
+ const std::vector<Node>& nodes);
/** Helper method to collect all elements of a set. */
static void collectSet(std::set<Term>& set,
*/
std::string getProof() const;
+ /**
+ * Get learned literals
+ *
+ * @return a list of literals that were learned at top-level. In other words,
+ * these are literals that are entailed by the current set of assertions.
+ */
+ std::vector<Term> getLearnedLiterals() const;
+
/**
* Get the value of the given term in the current model.
*
*/
// TODO: void echo(std::ostream& out, String str)
+ /**
+ * Get a list of literals that are entailed by the current set of assertions
+ * SMT-LIB:
+ * {@code
+ * ( get-learned-literals )
+ * }
+ * @return the list of learned literals
+ */
+ public Term[] getLearnedLiterals() {
+ long[] retPointers = getLearnedLiterals(pointer);
+ return Utils.getTerms(this, retPointers);
+ }
+
+ private native long[] getLearnedLiterals(long pointer);
+
/**
* Get the list of asserted formulas.
* SMT-LIB:
CVC5_JAVA_API_TRY_CATCH_END(env);
}
+/*
+ * Class: io_github_cvc5_api_Solver
+ * Method: getLearnedLiterals
+ * Signature: (J)[J
+ */
+JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Solver_getLearnedLiterals(
+ JNIEnv* env, jobject, jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Solver* solver = reinterpret_cast<Solver*>(pointer);
+ std::vector<Term> assertions = solver->getLearnedLiterals();
+ jlongArray ret = getPointersFromObjects<Term>(env, assertions);
+ return ret;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
/*
* Class: io_github_cvc5_api_Solver
* Method: getAssertions
Term term, bint glbl) except +
Term defineFunsRec(vector[Term]& funs, vector[vector[Term]]& bound_vars,
vector[Term]& terms, bint glbl) except +
+ vector[Term] getLearnedLiterals() except +
vector[Term] getAssertions() except +
string getInfo(const string& flag) except +
string getOption(string& option) except +
for t in terms:
vf.push_back((<Term?> t).cterm)
+ def getLearnedLiterals(self):
+ """Get a list of literals that are entailed by the current set of assertions
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( get-learned-literals )
+
+ :return: the list of literals
+ """
+ lits = []
+ for a in self.csolver.getLearnedLiterals():
+ term = Term(self)
+ term.cterm = a
+ lits.append(term)
+ return lits
+
def getAssertions(self):
"""Get the list of asserted formulas.
name = "values"
help = "Block models based on the concrete model values for the free variables."
+[[option]]
+ name = "produceLearnedLiterals"
+ category = "regular"
+ long = "produce-learned-literals"
+ type = "bool"
+ default = "false"
+ help = "produce learned literals, support get-learned-literals"
+
[[option]]
name = "produceProofs"
category = "regular"
| /* get-difficulty */
GET_DIFFICULTY_TOK { PARSER_STATE->checkThatLogicIsSet(); }
{ cmd->reset(new GetDifficultyCommand); }
+ | /* get-learned-literals */
+ GET_LEARNED_LITERALS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+ { cmd->reset(new GetLearnedLiteralsCommand); }
| /* push */
PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
( k=INTEGER_LITERAL
GET_UNSAT_ASSUMPTIONS_TOK : 'get-unsat-assumptions';
GET_UNSAT_CORE_TOK : 'get-unsat-core';
GET_DIFFICULTY_TOK : 'get-difficulty';
+GET_LEARNED_LITERALS_TOK : { !PARSER_STATE->strictModeEnabled() }? 'get-learned-literals';
EXIT_TOK : 'exit';
RESET_TOK : 'reset';
RESET_ASSERTIONS_TOK : 'reset-assertions';
printUnknownCommand(out, "get-difficulty");
}
+void Printer::toStreamCmdGetLearnedLiterals(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-learned-literals");
+}
+
void Printer::toStreamCmdGetAssertions(std::ostream& out) const
{
printUnknownCommand(out, "get-assertions");
/** Print get-difficulty command */
virtual void toStreamCmdGetDifficulty(std::ostream& out) const;
+ /** Print get-learned-literals command */
+ virtual void toStreamCmdGetLearnedLiterals(std::ostream& out) const;
+
/** Print get-assertions command */
virtual void toStreamCmdGetAssertions(std::ostream& out) const;
out << "(get-difficulty)" << std::endl;
}
+void Smt2Printer::toStreamCmdGetLearnedLiterals(std::ostream& out) const
+{
+ out << "(get-learned-literals)" << std::endl;
+}
+
void Smt2Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
const std::string& logic) const
{
/** Print get-difficulty command */
void toStreamCmdGetDifficulty(std::ostream& out) const override;
+ /** Print get-learned-literals command */
+ void toStreamCmdGetLearnedLiterals(std::ostream& out) const override;
+
/** Print get-assertions command */
void toStreamCmdGetAssertions(std::ostream& out) const override;
return cdp.getProofFor(fnode);
}
-const std::unordered_set<Node>& PropEngine::getLearnedZeroLevelLiterals() const
+std::vector<Node> PropEngine::getLearnedZeroLevelLiterals() const
{
return d_theoryProxy->getLearnedZeroLevelLiterals();
}
std::shared_ptr<ProofNode> getRefutation();
/** Get the zero-level assertions */
- const std::unordered_set<Node>& getLearnedZeroLevelLiterals() const;
+ std::vector<Node> getLearnedZeroLevelLiterals() const;
private:
/** Dump out the satisfying assignment (after SAT result) */
d_skdm(skdm),
d_zll(nullptr)
{
- bool trackTopLevelLearned = isOutputOn(OutputTag::LEARNED_LITS);
+ bool trackTopLevelLearned = isOutputOn(OutputTag::LEARNED_LITS)
+ || options().smt.produceLearnedLiterals;
if (trackTopLevelLearned)
{
d_zll = std::make_unique<ZeroLevelLearner>(env, propEngine);
void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); }
-const std::unordered_set<Node>& TheoryProxy::getLearnedZeroLevelLiterals() const
+std::vector<Node> TheoryProxy::getLearnedZeroLevelLiterals() const
{
- Assert(d_zll != nullptr);
- return d_zll->getLearnedZeroLevelLiterals();
+ if (d_zll != nullptr)
+ {
+ return d_zll->getLearnedZeroLevelLiterals();
+ }
+ return {};
}
} // namespace prop
void preRegister(Node n) override;
/** Get the zero-level assertions */
- const std::unordered_set<Node>& getLearnedZeroLevelLiterals() const;
+ std::vector<Node> getLearnedZeroLevelLiterals() const;
private:
/** The prop engine we are using. */
ZeroLevelLearner::ZeroLevelLearner(Env& env, PropEngine* propEngine)
: EnvObj(env),
d_propEngine(propEngine),
+ d_levelZeroAsserts(userContext()),
+ d_levelZeroAssertsLearned(userContext()),
d_nonZeroAssert(context(), false),
+ d_ppnAtoms(userContext()),
+ d_pplAtoms(userContext()),
d_assertNoLearnCount(0)
{
}
void ZeroLevelLearner::getAtoms(TNode a,
std::unordered_set<TNode>& visited,
- std::unordered_set<TNode>& ppLits)
+ NodeSet& ppLits)
{
std::vector<TNode> visit;
TNode cur;
const std::vector<Node>& ppl)
{
d_assertNoLearnCount = 0;
- d_ppnAtoms.clear();
// Copy the preprocessed assertions and skolem map information directly
// Also, compute the set of literals in the preprocessed assertions
std::unordered_set<TNode> visited;
}
}
-const std::unordered_set<Node>& ZeroLevelLearner::getLearnedZeroLevelLiterals()
- const
+std::vector<Node> ZeroLevelLearner::getLearnedZeroLevelLiterals() const
{
- return d_levelZeroAssertsLearned;
+ std::vector<Node> ret;
+ for (const Node& n : d_levelZeroAssertsLearned)
+ {
+ ret.push_back(n);
+ }
+ return ret;
}
} // namespace prop
void notifyAsserted(TNode assertion);
/** Get the zero-level assertions */
- const std::unordered_set<Node>& getLearnedZeroLevelLiterals() const;
+ std::vector<Node> getLearnedZeroLevelLiterals() const;
private:
static void getAtoms(TNode a,
std::unordered_set<TNode>& visited,
- std::unordered_set<TNode>& ppLits);
+ NodeSet& ppLits);
/** The prop engine we are using. */
PropEngine* d_propEngine;
/** Set of literals that hold at level 0 */
- std::unordered_set<TNode> d_levelZeroAsserts;
+ NodeSet d_levelZeroAsserts;
/** Set of learnable literals that hold at level 0 */
- std::unordered_set<Node> d_levelZeroAssertsLearned;
+ NodeSet d_levelZeroAssertsLearned;
/** Whether we have seen an assertion level > 0 */
context::CDO<bool> d_nonZeroAssert;
/** Preprocessed literals that are not learned */
- std::unordered_set<TNode> d_ppnAtoms;
+ NodeSet d_ppnAtoms;
/** Already learned TEMPORARY */
- std::unordered_set<TNode> d_pplAtoms;
+ NodeSet d_pplAtoms;
/** Current counter of assertions */
size_t d_assertNoLearnCount;
Printer::getPrinter(language)->toStreamCmdGetDifficulty(out);
}
+/* -------------------------------------------------------------------------- */
+/* class GetLearnedLiteralsCommand */
+/* -------------------------------------------------------------------------- */
+
+GetLearnedLiteralsCommand::GetLearnedLiteralsCommand() {}
+void GetLearnedLiteralsCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ d_result = solver->getLearnedLiterals();
+
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (api::CVC5ApiRecoverableException& e)
+ {
+ d_commandStatus = new CommandRecoverableFailure(e.what());
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+void GetLearnedLiteralsCommand::printResult(std::ostream& out) const
+{
+ if (!ok())
+ {
+ this->Command::printResult(out);
+ }
+ else
+ {
+ out << "(" << std::endl;
+ for (const api::Term& lit : d_result)
+ {
+ out << lit << std::endl;
+ }
+ out << ")" << std::endl;
+ }
+}
+
+const std::vector<api::Term>& GetLearnedLiteralsCommand::getLearnedLiterals()
+ const
+{
+ return d_result;
+}
+
+Command* GetLearnedLiteralsCommand::clone() const
+{
+ GetLearnedLiteralsCommand* c = new GetLearnedLiteralsCommand;
+ c->d_result = d_result;
+ return c;
+}
+
+std::string GetLearnedLiteralsCommand::getCommandName() const
+{
+ return "get-learned-literals";
+}
+
+void GetLearnedLiteralsCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ Language language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetLearnedLiterals(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class GetAssertionsCommand */
/* -------------------------------------------------------------------------- */
std::map<api::Term, api::Term> d_result;
};
+class CVC5_EXPORT GetLearnedLiteralsCommand : public Command
+{
+ public:
+ GetLearnedLiteralsCommand();
+ const std::vector<api::Term>& getLearnedLiterals() const;
+
+ void invoke(api::Solver* solver, SymbolManager* sm) override;
+ void printResult(std::ostream& out) const override;
+
+ Command* clone() const override;
+ std::string getCommandName() const override;
+ void toStream(std::ostream& out,
+ int toDepth = -1,
+ size_t dag = 1,
+ Language language = Language::LANG_AUTO) const override;
+
+ protected:
+ /** the result of the get learned literals call */
+ std::vector<api::Term> d_result;
+};
+
class CVC5_EXPORT GetAssertionsCommand : public Command
{
protected:
Node SolverEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
+std::vector<Node> SolverEngine::getLearnedLiterals()
+{
+ Trace("smt") << "SMT getLearnedLiterals()" << std::endl;
+ SolverEngineScope smts(this);
+ // note that the default mode for learned literals is via the prop engine,
+ // although other modes could use the preprocessor
+ PropEngine* pe = getPropEngine();
+ Assert(pe != nullptr);
+ return pe->getLearnedZeroLevelLiterals();
+}
+
void SolverEngine::checkProof()
{
Assert(d_env->getOptions().smt.produceProofs);
/** When using separation logic, obtain the expression for nil. */
Node getSepNilExpr();
+ /**
+ * Get the list of top-level learned literals that are entailed by the current
+ * set of assertions.
+ *
+ * TODO (wishue #104): implement for different modes
+ */
+ std::vector<Node> getLearnedLiterals();
+
/**
* Get an aspect of the current SMT execution environment.
* @throw OptionException
regress1/fmf/sort-inf-int.smt2
regress1/fmf/with-ind-104-core.smt2
regress1/gensys_brn001.smt2
+ regress1/get-learned-literals.smt2
regress1/ho/bug_freeVar_BDD_General_data_270.p
regress1/ho/bug_freevar_PHI004^4-delta.smt2
regress1/ho/bound_var_bug.p
--- /dev/null
+; SCRUBBER: sed -e 's/(>=.*/learned-ineq/'
+; EXPECT: sat
+; EXPECT: (
+; EXPECT: learned-ineq
+; EXPECT: learned-ineq
+; EXPECT: )
+(set-logic ALL)
+(set-option :produce-learned-literals true)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+
+(assert (> x 5))
+(assert (< y 4))
+(assert (or (< x y) (> z 0)))
+(check-sat)
+(get-learned-literals)
\ No newline at end of file
Term ten = d_solver.mkInteger(10);
Term f0 = d_solver.mkTerm(GEQ, x, ten);
Term f1 = d_solver.mkTerm(GEQ, zero, x);
+ d_solver.assertFormula(f0);
+ d_solver.assertFormula(f1);
d_solver.checkSat();
std::map<Term, Term> dmap;
ASSERT_NO_THROW(dmap = d_solver.getDifficulty());
}
}
+TEST_F(TestApiBlackSolver, getLearnedLiterals)
+{
+ d_solver.setOption("produce-learned-literals", "true");
+ // cannot ask before a check sat
+ ASSERT_THROW(d_solver.getLearnedLiterals(), CVC5ApiException);
+ d_solver.checkSat();
+ ASSERT_NO_THROW(d_solver.getLearnedLiterals());
+}
+
+TEST_F(TestApiBlackSolver, getLearnedLiterals2)
+{
+ d_solver.setOption("produce-learned-literals", "true");
+ Sort intSort = d_solver.getIntegerSort();
+ Term x = d_solver.mkConst(intSort, "x");
+ Term y = d_solver.mkConst(intSort, "y");
+ Term zero = d_solver.mkInteger(0);
+ Term ten = d_solver.mkInteger(10);
+ Term f0 = d_solver.mkTerm(GEQ, x, ten);
+ Term f1 = d_solver.mkTerm(
+ OR, d_solver.mkTerm(GEQ, zero, x), d_solver.mkTerm(GEQ, y, zero));
+ d_solver.assertFormula(f0);
+ d_solver.assertFormula(f1);
+ d_solver.checkSat();
+ ASSERT_NO_THROW(d_solver.getLearnedLiterals());
+}
+
TEST_F(TestApiBlackSolver, getValue1)
{
d_solver.setOption("produce-models", "false");
Term ten = d_solver.mkInteger(10);
Term f0 = d_solver.mkTerm(GEQ, x, ten);
Term f1 = d_solver.mkTerm(GEQ, zero, x);
+ d_solver.assertFormula(f0);
+ d_solver.assertFormula(f1);
d_solver.checkSat();
Map<Term, Term> dmap = d_solver.getDifficulty();
// difficulty should map assertions to integer values
}
}
+ @Test
+ void getLearnedLiterals() {
+ d_solver.setOption("produce-learned-literals", "true");
+ // cannot ask before a check sat
+ assertThrows(CVC5ApiException.class, () -> d_solver.getLearnedLiterals());
+ d_solver.checkSat();
+ assertDoesNotThrow(() -> d_solver.getLearnedLiterals());
+ }
+
+ @Test
+ void getLearnedLiterals2() {
+ d_solver.setOption("produce-learned-literals", "true");
+ Sort intSort = d_solver.getIntegerSort();
+ Term x = d_solver.mkConst(intSort, "x");
+ Term y = d_solver.mkConst(intSort, "y");
+ Term zero = d_solver.mkInteger(0);
+ Term ten = d_solver.mkInteger(10);
+ Term f0 = d_solver.mkTerm(GEQ, x, ten);
+ Term f1 = d_solver.mkTerm(
+ OR, d_solver.mkTerm(GEQ, zero, x), d_solver.mkTerm(GEQ, y, zero));
+ d_solver.assertFormula(f0);
+ d_solver.assertFormula(f1);
+ d_solver.checkSat();
+ assertDoesNotThrow(() -> d_solver.getLearnedLiterals());
+ }
+
@Test void getValue1()
{
d_solver.setOption("produce-models", "false");
res = solver.checkSat()
assert res.isUnsat()
+def test_learned_literals(solver):
+ solver.setOption("produce-learned-literals", "true")
+ with pytest.raises(RuntimeError):
+ solver.getLearnedLiterals()
+ solver.checkSat()
+ solver.getLearnedLiterals()
+
+def test_learned_literals2(solver):
+ solver.setOption("produce-learned-literals", "true")
+ intSort = solver.getIntegerSort()
+ x = solver.mkConst(intSort, "x")
+ y = solver.mkConst(intSort, "y")
+ zero = solver.mkInteger(0)
+ ten = solver.mkInteger(10)
+ f0 = solver.mkTerm(Kind.Geq, x, ten)
+ f1 = solver.mkTerm(Kind.Or, solver.mkTerm(Kind.Geq, zero, x), solver.mkTerm(Kind.Geq, y, zero))
+ solver.assertFormula(f0)
+ solver.assertFormula(f1)
+ solver.checkSat()
+ solver.getLearnedLiterals()
+
def test_get_value1(solver):
solver.setOption("produce-models", "false")
projects / cvc5.git / commitdiff