This makes subsolvers answer "unknown" instead of "unsat" when solving SyGuS inputs, by setting unknown when a SyGuS input is solved instead of asserting the negation of the input. Knowing whether the call was successful is simply obtained by calling getSynthSolutions.
This will allow for multiple solutions for the same conjecture.
Trace("sygus-infer") << "*** Check sat..." << std::endl;
Result r = rrSygus->checkSat();
Trace("sygus-infer") << "...result : " << r << std::endl;
- if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+ // get the synthesis solutions
+ std::map<Node, Node> synth_sols;
+ if (!rrSygus->getSubsolverSynthSolutions(synth_sols))
{
// failed, conjecture was infeasible
return false;
}
- // get the synthesis solutions
- std::map<Node, Node> synth_sols;
- bool sinferSol = rrSygus->getSubsolverSynthSolutions(synth_sols);
- AlwaysAssert(sinferSol) << "Failed to get solutions for sygus-inference";
std::vector<Node> final_ff;
std::vector<Node> final_ff_sol;
Result r = d_subsolver->checkSat();
Trace("sygus-abduct") << " SolverEngine::getAbduct result: " << r
<< std::endl;
- if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ // get the synthesis solution
+ std::map<Node, Node> sols;
+ // use the "getSubsolverSynthSolutions" interface, since we asserted the
+ // internal form of the SyGuS conjecture and used check-sat.
+ if (d_subsolver->getSubsolverSynthSolutions(sols))
{
- // get the synthesis solution
- std::map<Node, Node> sols;
- // use the "getSubsolverSynthSolutions" interface, since we asserted the
- // internal form of the SyGuS conjecture and used check-sat.
- d_subsolver->getSubsolverSynthSolutions(sols);
Assert(sols.size() == 1);
std::map<Node, Node>::iterator its = sols.find(d_sssf);
if (its != sols.end())
d_env.verbose(2) << "solving..." << std::endl;
Trace("smt") << "SmtSolver::check(): running check" << endl;
Result result = d_propEngine->checkSat();
+ Trace("smt") << "SmtSolver::check(): result " << result << std::endl;
rm->endCall();
Trace("limit") << "SmtSolver::check(): cumulative millis "
query.push_back(d_conj);
r = d_smtSolver.checkSatisfiability(as, query, false);
}
- // Check that synthesis solutions satisfy the conjecture
- if (options().smt.checkSynthSol
- && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ // The result returned by the above call is typically "unknown", which may
+ // or may not correspond to a state in which we solved the conjecture
+ // successfully. Instead we call getSynthSolutions below. If this returns
+ // true, then we were successful. In this case, we set the result to "unsat",
+ // since the synthesis conjecture was negated when asserted to the subsolver.
+ //
+ // This behavior is done for 2 reasons:
+ // (1) if we do not negate the synthesis conjecture, the subsolver in some
+ // cases cannot answer "sat", e.g. in the presence of recursive function
+ // definitions. Instead the SyGuS language standard itself indicates that
+ // a correct solution for a conjecture is one where the synthesis conjecture
+ // is *T-valid* (in the presence of defined recursive functions). In other
+ // words, a SyGuS query asks to prove that the conjecture is valid when
+ // witnessed by the given solution.
+ // (2) we do not want the solver to explicitly answer "unsat" by giving an
+ // unsatisfiable set of formulas to the underlying PropEngine, or otherwise
+ // we will not be able to ask for further solutions. This is critical for
+ // incremental solving where multiple solutions are returned for the same
+ // set of constraints. Thus, the internal SyGuS solver will mark unknown
+ // with IncompleteId::QUANTIFIERS_SYGUS_SOLVED. Furthermore, this id may be
+ // overwritten by other means of incompleteness, so we cannot rely on this
+ // identifier being the final reason for unknown.
+ //
+ // Thus, we use getSynthSolutions as means of knowing the conjecture was
+ // solved.
+ std::map<Node, Node> sol_map;
+ if (getSynthSolutions(sol_map))
+ {
+ // if we have solutions, we return "unsat" by convention
+ r = Result(Result::UNSAT);
+ // Check that synthesis solutions satisfy the conjecture
+ if (options().smt.checkSynthSol)
+ {
+ checkSynthSolution(as, sol_map);
+ }
+ }
+ else
{
- checkSynthSolution(as);
+ // otherwise, we return "unknown"
+ r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
}
return r;
}
return true;
}
-void SygusSolver::checkSynthSolution(Assertions& as)
+void SygusSolver::checkSynthSolution(Assertions& as,
+ const std::map<Node, Node>& sol_map)
{
if (isVerboseOn(1))
{
verbose(1) << "SyGuS::checkSynthSolution: checking synthesis solution"
<< std::endl;
}
- std::map<Node, Node> sol_map;
- // Get solutions and build auxiliary vectors for substituting
- if (!getSynthSolutions(sol_map))
- {
- InternalError()
- << "SygusSolver::checkSynthSolution(): No solution to check!";
- return;
- }
if (sol_map.empty())
{
InternalError() << "SygusSolver::checkSynthSolution(): Got empty solution!";
* conjecture in which the functions-to-synthesize have been replaced by the
* synthesized solutions, which is a quantifier-free formula, is
* unsatisfiable. If not, then the found solutions are wrong.
+ *
+ * @param as The background assertions, which may include define-fun and
+ * define-fun-rec,
+ * @param sol_map Map from functions-to-synthesize to their solution (of the
+ * same type) for the asserted synthesis conjecture.
*/
- void checkSynthSolution(Assertions& as);
+ void checkSynthSolution(Assertions& as, const std::map<Node, Node>& solMap);
/**
* Expand definitions in sygus datatype tn, which ensures that all
* sygus constructors that are used to build values of sygus datatype
return "QUANTIFIERS_RECORDED_INST";
case IncompleteId::QUANTIFIERS_MAX_INST_ROUNDS:
return "QUANTIFIERS_MAX_INST_ROUNDS";
+ case IncompleteId::QUANTIFIERS_SYGUS_SOLVED:
+ return "QUANTIFIERS_SYGUS_SOLVED";
case IncompleteId::SEP: return "SEP";
case IncompleteId::SETS_RELS_CARD: return "SETS_RELS_CARD";
case IncompleteId::STRINGS_LOOP_SKIP: return "STRINGS_LOOP_SKIP";
QUANTIFIERS_RECORDED_INST,
// incomplete due to limited number of allowed instantiation rounds
QUANTIFIERS_MAX_INST_ROUNDS,
+ // we solved a negated synthesis conjecture and will terminate as a subsolver
+ // with unknown
+ QUANTIFIERS_SYGUS_SOLVED,
// incomplete due to separation logic
SEP,
// relations were used in combination with set cardinality constraints
return "QUANTIFIERS_SYGUS_EXCLUDE_CURRENT";
case InferenceId::QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT:
return "QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT";
- case InferenceId::QUANTIFIERS_SYGUS_SI_SOLVED:
- return "QUANTIFIERS_SYGUS_SI_SOLVED";
- case InferenceId::QUANTIFIERS_SYGUS_SAMPLE_TRUST_SOLVED:
- return "QUANTIFIERS_SYGUS_SAMPLE_TRUST_SOLVED";
- case InferenceId::QUANTIFIERS_SYGUS_VERIFY_SOLVED:
- return "QUANTIFIERS_SYGUS_VERIFY_SOLVED";
case InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA:
return "QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA";
case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB:
QUANTIFIERS_SYGUS_EXCLUDE_CURRENT,
// manual exclusion of a current solution for sygus-stream
QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT,
- // Q where Q was solved by a subcall to the single invocation module
- QUANTIFIERS_SYGUS_SI_SOLVED,
- // Q where Q was (trusted) solved by sampling
- QUANTIFIERS_SYGUS_SAMPLE_TRUST_SOLVED,
- // Q where Q was solved by a verification subcall
- QUANTIFIERS_SYGUS_VERIFY_SOLVED,
// ~Q where Q is a PBE conjecture with conflicting examples
QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA,
// unif+pi symmetry breaking between multiple enumerators
bool SynthConjecture::doCheck()
{
+ if (d_hasSolution)
+ {
+ return true;
+ }
if (isSingleInvocation())
{
// We now try to solve with the single invocation solver, which may or may
if (d_ceg_si->solve())
{
d_hasSolution = true;
- // the conjecture has a solution, so its negation holds
- Node qn = d_quant.negate();
- d_qim.addPendingLemma(qn, InferenceId::QUANTIFIERS_SYGUS_SI_SOLVED);
+ // the conjecture has a solution, we set incomplete
+ d_qim.setIncomplete(IncompleteId::QUANTIFIERS_SYGUS_SOLVED);
}
return true;
}
Assert(d_master != nullptr);
- Assert(!d_hasSolution);
// get the list of terms that the master strategy is interested in
std::vector<Node> terms;
if (options().quantifiers.cegisSample == options::CegisSampleMode::TRUST)
{
// we have that the current candidate passed a sample test
- // since we trust sampling in this mode, we assert there is no
- // counterexample to the conjecture here.
- Node qn = d_quant.negate();
- d_qim.addPendingLemma(qn,
- InferenceId::QUANTIFIERS_SYGUS_SAMPLE_TRUST_SOLVED);
+ // since we trust sampling in this mode, we assume there is a solution here
+ // and set incomplete.
+ d_hasSolution = true;
+ d_qim.setIncomplete(IncompleteId::QUANTIFIERS_SYGUS_SOLVED);
recordSolution(candidate_values);
return true;
}
d_hasSolution = false;
return false;
}
- // Use lemma to terminate with "unsat", this is justified by the verification
- // check above, which confirms the synthesis conjecture is solved.
- Node qn = d_quant.negate();
- d_qim.addPendingLemma(qn, InferenceId::QUANTIFIERS_SYGUS_VERIFY_SOLVED);
+ // We set incomplete and terminate with unknown.
+ d_qim.setIncomplete(IncompleteId::QUANTIFIERS_SYGUS_SOLVED);
return true;
}
d_relManager->getDifficultyMap(dmap);
}
+theory::IncompleteId TheoryEngine::getIncompleteId() const
+{
+ return d_incompleteId.get();
+}
+
Node TheoryEngine::getModelValue(TNode var) {
if (var.isConst())
{
*/
void getDifficultyMap(std::map<Node, Node>& dmap);
+ /** Get incomplete id, valid immediately after an `unknown` response. */
+ theory::IncompleteId getIncompleteId() const;
+
/**
* Forwards an entailment check according to the given theoryOfMode.
* See theory.h for documentation on entailmentCheck().
projects / cvc5.git / commitdiff