Skip to content

Commit

Permalink
minor fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
Johannes Schoisswohl committed Feb 11, 2021
1 parent 18b2f03 commit 64e667d
Show file tree
Hide file tree
Showing 7 changed files with 152 additions and 81 deletions.
14 changes: 9 additions & 5 deletions Inferences/TheoryInstAndSimp.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@
*/

#if VZ3
#define DEBUG(...) // DBG(__VA_ARGS__)
#define DEBUG(...) //DBG(__VA_ARGS__)

#define DPRINT 0

Expand Down Expand Up @@ -446,13 +446,14 @@ void TheoryInstAndSimp::filterUninterpretedPartialFunctionDeep(Stack<Literal*>&
}

void TheoryInstAndSimp::ConstantCache::reset()
{ for (auto x : _inner) x.reset(); }
{ for (auto& x : _inner) x.reset(); }

Term* TheoryInstAndSimp::ConstantCache::freshConstant(unsigned sort)
{
if (_inner.size() <= sort) {
_inner.reserve(sort + 1);
while (_inner.size() <= sort) {
DEBUG("new constant cache for sort ", _inner.size());
_inner.push(SortedConstantCache());
}
}
Expand All @@ -464,10 +465,11 @@ void TheoryInstAndSimp::ConstantCache::SortedConstantCache::reset()

Term* TheoryInstAndSimp::ConstantCache::SortedConstantCache::freshConstant(const char* prefix, unsigned sort)
{
if (_constants.size() >= _used) {
if (_constants.size() == _used) {
unsigned sym = env.signature->addFreshFunction(0, prefix);
env.signature->getFunction(sym)
->setType(OperatorType::getConstantsType(sort));
DEBUG("new constant for sort ", sort, ": ", *env.signature->getFunction(sym));
_constants.push(Term::createConstant(sym));
}
return _constants[_used++];
Expand Down Expand Up @@ -565,7 +567,7 @@ Option<Substitution> TheoryInstAndSimp::instantiateGeneralised(
ASS_EQ(res, SATSolver::UNSATISFIABLE)

Set<TermList> usedDefs;
for (auto x : _solver->failedAssumptions()) {
for (auto& x : _solver->failedAssumptions()) {
definitionLiterals
.tryGet(x)
.andThen([&](TermList t)
Expand Down Expand Up @@ -649,9 +651,10 @@ VirtualIterator<Solution> TheoryInstAndSimp::getSolutions(Stack<Literal*> const&
BYPASSING_ALLOCATOR;

auto skolemized = skolemize(iterTraits(getConcatenatedIterator(
iterTraits(theoryLiterals.iterFifo()),
theoryLiterals.iterFifo(),
guards.iterFifo()
)));
DEBUG("skolemized: ", iterTraits(skolemized.lits.iterFifo()).map([&](SATLiteral l){ return _naming.toFO(l)->toString(); }).collect<Stack>())

// now we can call the solver
SATSolver::Status status = _solver->solveUnderAssumptions(skolemized.lits, 0, false);
Expand Down Expand Up @@ -889,6 +892,7 @@ Stack<Literal*> filterLiterals(Stack<Literal*> lits, Options::TheoryInstSimp mod
case Options::TheoryInstSimp::OFF:
ASSERTION_VIOLATION
}
ASSERTION_VIOLATION
}

unsigned getFreshVar(Clause& clause)
Expand Down
2 changes: 2 additions & 0 deletions Inferences/TheoryInstAndSimp.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -138,7 +138,9 @@ class TheoryInstAndSimp
Options::TheoryInstSimp const _mode;
bool const _thiTautologyDeletion;
SAT2FO _naming;
volatile char padding00[1024];
Z3Interfacing* _solver;
volatile char padding01[1024];
Map<unsigned, bool> _supportedSorts;
bool _generalisation;
ConstantCache _instantiationConstants;
Expand Down
2 changes: 1 addition & 1 deletion Lib/BiMap.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ class BiMap : Map<A,B, HashA>, Map<B, A, HashB> {
return Into::getOrInit(key, [&]() {
auto val = init();
From::insert(val, key);
return std::move(val);
return val;
});
}

Expand Down
100 changes: 54 additions & 46 deletions SAT/Z3Interfacing.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,8 @@
#include "Indexing/TermSharing.hpp"
#include "Z3Interfacing.hpp"

#define DEBUG(...) // DBG(__VA_ARGS__)
#define DEBUG(...) //DBG(__VA_ARGS__)
#define TRACE_Z3 0
namespace Lib {

template<>
Expand Down Expand Up @@ -119,7 +120,7 @@ Z3Interfacing::Z3Interfacing(SAT2FO& s2f, bool showZ3, bool unsatCore):
_solver.check();
),
_solver.get_model())),
_assumptions(_context),
_assumptions(),
_showZ3(showZ3),
_unsatCore(unsatCore)
{
Expand All @@ -128,7 +129,6 @@ Z3Interfacing::Z3Interfacing(SAT2FO& s2f, bool showZ3, bool unsatCore):
_solver.reset();

z3::set_param("rewriter.expand_store_eq", "true");
//z3::set_param("trace", "true");

z3::params p(_context);
p.set("model.compact", false); // keeps z3 from compressing its model. ~50% of the runtime of get_model is spent doing that otherwise
Expand All @@ -138,7 +138,12 @@ Z3Interfacing::Z3Interfacing(SAT2FO& s2f, bool showZ3, bool unsatCore):
//p.set(":smtlib2-compliant",true);
_solver.set(p);
Z3_set_error_handler(_context, handleZ3Error);
//Z3_enable_trace("memory");

#if TRACE_Z3
p.set("trace", "true");
Z3_enable_trace("memory");
Z3_enable_trace("datatype");
#endif // TRACE_Z3
}

char const* Z3Interfacing::z3_full_version()
Expand Down Expand Up @@ -188,20 +193,20 @@ void Z3Interfacing::addClause(SATClause* cl)
void Z3Interfacing::retractAllAssumptions()
{
_assumptionLookup.clear();
_assumptions.resize(0);
_assumptions.truncate(0);
}

void Z3Interfacing::addAssumption(SATLiteral lit)
{
CALL("Z3Interfacing::addAssumption");

auto pushAssumption = [this](SATLiteral lit) -> z3::expr
auto pushAssumption = [&](SATLiteral lit) -> z3::expr
{
auto repr = getRepresentation(lit);
for (auto def : repr.defs)
_assumptions.push_back(def);
for (auto& def : repr.defs)
_assumptions.push(def);

_assumptions.push_back(repr.expr);
_assumptions.push(repr.expr);
return repr.expr;
};

Expand Down Expand Up @@ -238,39 +243,37 @@ SATSolver::Status Z3Interfacing::solve()
BYPASSING_ALLOCATOR;
DEBUG("assumptions: ", _assumptions);

z3::check_result result = _solver.check(_assumptions.size(), _assumptions.begin());

z3::check_result result = _assumptions.empty() ? _solver.check() : _solver.check(_assumptions);


if(_showZ3){
env.beginOutput();
env.out() << "[Z3] solve result: " << result << std::endl;
env.endOutput();
}
if(_showZ3){
env.beginOutput();
env.out() << "[Z3] solve result: " << result << std::endl;
env.endOutput();
}

if (_unsatCore) {
auto core = _solver.unsat_core();
for (auto phi : core) {
_assumptionLookup
.tryGet(phi)
.andThen([this](SATLiteral l)
{ _failedAssumptionBuffer.push(l); });
}
if (_unsatCore) {
auto core = _solver.unsat_core();
for (auto phi : core) {
_assumptionLookup
.tryGet(phi)
.andThen([this](SATLiteral l)
{ _failedAssumptionBuffer.push(l); });
}
}

switch (result) {
case z3::check_result::unsat:
_status = UNSATISFIABLE;
break;
case z3::check_result::sat:
_status = SATISFIABLE;
_model = _solver.get_model();
break;
case z3::check_result::unknown:
_status = UNKNOWN;
break;
default: ASSERTION_VIOLATION;
}
switch (result) {
case z3::check_result::unsat:
_status = UNSATISFIABLE;
break;
case z3::check_result::sat:
_status = SATISFIABLE;
_model = _solver.get_model();
break;
case z3::check_result::unknown:
_status = UNKNOWN;
break;
default: ASSERTION_VIOLATION;
}

return _status;
}
Expand Down Expand Up @@ -534,13 +537,16 @@ void Z3Interfacing::createTermAlgebra(TermAlgebra& start)

#if !INT_IDENTS
auto new_string_symobl = [&](vstring str)
{ return Z3_mk_string_symbol(_context, str.c_str()); };
{
return Z3_mk_string_symbol(_context, str.c_str());
};
#endif

// create the data needed for Z3_mk_datatypes(...)
Stack<Stack<Z3_constructor>> ctorss(tas.size());
Stack<Z3_constructor_list> ctorss_z3(tas.size());
Stack<Z3_symbol> sortNames(tas.size());

DEBUG("creating constructors: ");
for (auto ta : tas) {
_createdTermAlgebras.insert(ta->sort());
Expand Down Expand Up @@ -573,7 +579,7 @@ void Z3Interfacing::createTermAlgebra(TermAlgebra& start)
cons->createDiscriminator();
auto discrName = cons->discriminatorName().c_str();

DEBUG("\t", env.sorts->sortName(ta->sort()), "::", env.signature->getFunction(cons->functor())->name());
DEBUG("\t", env.sorts->sortName(ta->sort()), "::", env.signature->getFunction(cons->functor())->name(), ": ", env.signature->getFunction(cons->functor())->fnType()->toString());

ASS_EQ(argSortRefs.size(), cons->arity())
ASS_EQ( argSorts.size(), cons->arity())
Expand All @@ -587,10 +593,11 @@ void Z3Interfacing::createTermAlgebra(TermAlgebra& start)
#endif
Z3_mk_string_symbol(_context, discrName),
cons->arity(),
argNames.begin(),
argSorts.begin(),
argSortRefs.begin()
cons->arity() == 0 ? nullptr : argNames.begin(),
cons->arity() == 0 ? nullptr : argSorts.begin(),
cons->arity() == 0 ? nullptr : argSortRefs.begin()
));

}
ASS_EQ(ctors.size(), ta->nConstructors());

Expand Down Expand Up @@ -633,7 +640,6 @@ void Z3Interfacing::createTermAlgebra(TermAlgebra& start)

auto ctorId = FuncOrPredId::function(ctor->functor());
_toZ3.insert(ctorId, constr);
ASS(_toZ3.find(ctorId))
_fromZ3.insert(constr, ctorId);

if (ctor->hasDiscriminator()) {
Expand All @@ -651,7 +657,6 @@ void Z3Interfacing::createTermAlgebra(TermAlgebra& start)
}

// clean up

for (auto clist : ctorss_z3) {
Z3_del_constructor_list(_context, clist);
}
Expand All @@ -661,6 +666,7 @@ void Z3Interfacing::createTermAlgebra(TermAlgebra& start)
Z3_del_constructor(_context, ctor);
}
}

}

z3::func_decl const& Z3Interfacing::findConstructor(FuncId id_)
Expand Down Expand Up @@ -974,7 +980,8 @@ struct ToZ3Expr
z3::func_decl Z3Interfacing::z3Function(FuncOrPredId functor)
{
auto& self = *this;
return self._toZ3.tryGet(functor).toOwned()
return self._toZ3.tryGet(functor)
.toOwned()
.unwrapOrElse([&]() {
auto symb = functor.isPredicate ? env.signature->getPredicate(functor.id)
: env.signature->getFunction(functor.id);
Expand Down Expand Up @@ -1058,6 +1065,7 @@ SATClause* Z3Interfacing::getRefutation()
return PrimitiveProofRecordingSATSolver::getRefutation();
else {
ASS_EQ(_status, SATISFIABLE);
ASSERTION_VIOLATION
//TODO
// SATClauseList* prems = 0;
//
Expand Down
4 changes: 2 additions & 2 deletions SAT/Z3Interfacing.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ class Z3Interfacing : public PrimitiveProofRecordingSATSolver

virtual void addAssumption(SATLiteral lit) override;
virtual void retractAllAssumptions() override;
virtual bool hasAssumptions() const override { return !_assumptions.empty(); }
virtual bool hasAssumptions() const override { return !_assumptions.isEmpty(); }

virtual Status solveUnderAssumptions(const SATLiteralStack& assumps, unsigned conflictCountLimit, bool onlyProperSubusets) override;

Expand Down Expand Up @@ -223,7 +223,7 @@ class Z3Interfacing : public PrimitiveProofRecordingSATSolver
z3::model _model;


z3::expr_vector _assumptions;
Stack<z3::expr> _assumptions;
BiMap<SATLiteral, z3::expr> _assumptionLookup;
const bool _showZ3;
const bool _unsatCore;
Expand Down
Loading

0 comments on commit 64e667d

Please sign in to comment.