Skip to content

Commit

Permalink
start working on Monotonicity returning what it figured out in its SA…
Browse files Browse the repository at this point in the history 
…T call
  • Loading branch information
@quickbeam123
quickbeam123 committed Jul 29, 2024
1 parent a860f49 commit 4768334
Show file tree
Hide file tree
Showing 8 changed files with 74 additions and 60 deletions.
26 changes: 13 additions & 13 deletions FMB/FiniteModelBuilder.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -169,7 +169,7 @@ bool FiniteModelBuilder::reset(){
// Start from 1 as SAT solver variables are 1-based
unsigned offsets=1;
for(unsigned f=0; f<env.signature->functions();f++){
if(del_f[f]) continue;
if(del_f[f]) continue;
f_offsets[f]=offsets;
#if VTRACE_FMB
cout << "offset for " << f << " is " << offsets << " (arity is " << env.signature->functionArity(f) << ") " << endl;
Expand Down Expand Up @@ -2041,17 +2041,18 @@ void FiniteModelBuilder::onModelFound()
}
}

#if 0
//Evaluate removed functions and constants
unsigned maxf = env.signature->functions(); // model evaluation can add new constants
//bool unfinished=true;
//while(unfinished){
//unfinished=false;
unsigned f=maxf;
while(f > 0){
while(f > 0){
f--;
//cout << "Consider " << f << endl;
unsigned arity = env.signature->functionArity(f);
if(!del_f[f]) continue;
if(!del_f[f]) continue;
// For now, just skip unused functions!
if(env.signature->getFunction(f)->usageCnt()==0) continue;
//del_f[f]=false;
Expand All @@ -2063,7 +2064,7 @@ void FiniteModelBuilder::onModelFound()
//cout << def->toString() << endl;

ASS(def->isEquality());
Term* funApp = 0;
Term* funApp = 0;
Term* funDef = 0;

if(def->nthArgument(0)->term()->functor()==f){
Expand Down Expand Up @@ -2111,7 +2112,7 @@ void FiniteModelBuilder::onModelFound()

Substitution subst;
for(unsigned j=0;j<arity;j++){
TermList vs = env.signature->getFunction(f)->fnType()->arg(j);
TermList vs = env.signature->getFunction(f)->fnType()->arg(j);
unsigned vampireSrt = vs.term()->functor();
//cout << grounding[j] << " is " << model.getDomainConstant(grounding[j],vampireSrt)->toString() << endl;
subst.bind(vars[j],model.getDomainConstant(grounding[j],vampireSrt));
Expand Down Expand Up @@ -2139,15 +2140,14 @@ void FiniteModelBuilder::onModelFound()
}
catch(UserErrorException& exception){
//cout << "Setting unfinished" << endl;
//unfinished=true;
//unfinished=true;
//del_f[f]=true;
}
}
}
//}

//Evaluate removed propositions and predicates
#if 0
f=env.signature->predicates()-1;
while(f>0){
f--;
Expand All @@ -2163,7 +2163,7 @@ void FiniteModelBuilder::onModelFound()
//cout << "For " << env.signature->getPredicate(f)->name() << endl;
//cout << udef->toString() << endl;
//}
Formula* def = udef->getFormula();
Formula* def = udef->getFormula();
Literal* predApp = 0;
Formula* predDef = 0;
bool polarity = true;
Expand All @@ -2175,7 +2175,7 @@ void FiniteModelBuilder::onModelFound()
Formula* inner = def->qarg();
ASS(inner->connective()==Connective::IFF);
Formula* left = inner->left();
Formula* right = inner->right();
Formula* right = inner->right();

if(left->connective()==Connective::NOT){
polarity=!polarity;
Expand Down Expand Up @@ -2231,7 +2231,7 @@ void FiniteModelBuilder::onModelFound()
grounding[i]=1;
TermList vs = env.signature->getPredicate(f)->predType()->arg(i);
unsigned vampireSrt = vs.term()->functor();
unsigned dsrt = _sortedSignature->vampireToDistinctParent.get(vampireSrt);
unsigned dsrt = _sortedSignature->vampireToDistinctParent.get(vampireSrt);
p_signature_distinct[i] = dsrt;
}
grounding[arity-1]=0;
Expand All @@ -2251,9 +2251,9 @@ void FiniteModelBuilder::onModelFound()
}
else{
Substitution subst;
for(unsigned j=0;j<arity;j++){
for(unsigned j=0;j<arity;j++){
//cout << grounding[j] << " is " << model.getDomainConstant(grounding[j])->toString() << endl;
TermList vs = env.signature->getPredicate(f)->predType()->arg(j);
TermList vs = env.signature->getPredicate(f)->predType()->arg(j);
unsigned vampireSrt = vs.term()->functor();
subst.bind(vars[j],model.getDomainConstant(grounding[j],vampireSrt));
}
Expand All @@ -2265,7 +2265,7 @@ void FiniteModelBuilder::onModelFound()
if(!polarity) res=!res;
model.addPredicateDefinition(f,grounding,res);
}
catch(UserErrorException& exception){
catch(UserErrorException& exception){
// TODO order symbols for partial evaluation
}
}
Expand Down
26 changes: 12 additions & 14 deletions FMB/FiniteModelMultiSorted.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -218,7 +218,7 @@ std::string FiniteModelMultiSorted::toString()
if(frep >= 0){
cname = env.signature->functionName(frep);
}
cnames[s][i]=cname;
cnames[s][i]=cname;
modelStm << cname << ":" << sortName << ")." << endl;
}

Expand All @@ -227,7 +227,7 @@ std::string FiniteModelMultiSorted::toString()
modelStm << " ! [X:" << sortName << "] : (" << endl;
modelStm << " ";
for(unsigned i=1;i<=size;i++){
modelStm << "X = " << cnames[s][i];
modelStm << "X = " << cnames[s][i];
if(i<size) modelStm << " | ";
if(i==size) modelStm << endl;
else if(i%5==0) modelStm << endl << " ";
Expand Down Expand Up @@ -383,7 +383,7 @@ std::string FiniteModelMultiSorted::toString()
modelStm << "tff("<<prepend("declare_", name)<<",type,"<<name<<": (";
for(unsigned i=0;i<arity;i++){
TermList argST = sig->arg(i);
unsigned argS = argST.term()->functor();
unsigned argS = argST.term()->functor();
modelStm << env.signature->typeConName(argS);
if(i+1 < arity) modelStm << " * ";
}
Expand All @@ -408,7 +408,7 @@ std::string FiniteModelMultiSorted::toString()
else{
args[i]++;

//TODO could probably compute this directly, instead of via args
//TODO could probably compute this directly, instead of via args
// my mind isn't in the right place to do that now though!
unsigned var = offset;
unsigned mult=1;
Expand All @@ -432,7 +432,7 @@ std::string FiniteModelMultiSorted::toString()
if(j!=0) modelStm << ",";
TermList argSortT = sig->arg(j);
unsigned argSort = argSortT.term()->functor();
modelStm << cnames[argSort][args[j]];
modelStm << cnames[argSort][args[j]];
}
modelStm << ")";
if(res==0){
Expand All @@ -445,8 +445,6 @@ std::string FiniteModelMultiSorted::toString()
modelStm << endl << ")." << endl << endl;
}



return modelStm.str();
}

Expand All @@ -457,7 +455,7 @@ unsigned FiniteModelMultiSorted::evaluateGroundTerm(Term* term)
#if DEBUG_MODEL
cout << "evaluating ground term " << term->toString() << endl;
cout << "domain constant status " << isDomainConstant(term) << endl;
#endif
#endif
if(isDomainConstant(term)) return getDomainConstant(term).first;

unsigned arity = env.signature->functionArity(term->functor());
Expand Down Expand Up @@ -518,7 +516,7 @@ bool FiniteModelMultiSorted::evaluateGroundLiteral(Literal* lit)
var += mult*(args[i]-1);
unsigned s = sig->arg(i).term()->functor();
mult *=_sizes.get(s);
}
}

#if VDEBUG
if((lit->functor()+1)<p_offsets.size()) ASS_L(var,p_offsets[lit->functor()+1]);
Expand All @@ -527,14 +525,14 @@ bool FiniteModelMultiSorted::evaluateGroundLiteral(Literal* lit)

unsigned res = p_interpretation[var];
#if DEBUG_MODEL
cout << "res is " << res << " and polarity is " << lit->polarity() << endl;
cout << "res is " << res << " and polarity is " << lit->polarity() << endl;
#endif

if(res==0)
if(res==0)
USER_ERROR("Could not evaluate "+lit->toString()+", probably a partial model");

if(lit->polarity()) return (res==2);
else return (res==1);
else return (res==1);
}

bool FiniteModelMultiSorted::evaluate(Unit* unit)
Expand All @@ -560,13 +558,13 @@ bool FiniteModelMultiSorted::evaluate(Unit* unit)
/**
*
* TODO: This is recursive, which could be problematic in the long run
*
*
*/
bool FiniteModelMultiSorted::evaluate(Formula* formula,unsigned depth)
{
#if DEBUG_MODEL
for(unsigned i=0;i<depth;i++){ cout << "."; }
cout << "Evaluating..." << formula->toString() << endl;
cout << "Evaluating..." << formula->toString() << endl;
#endif

bool isAnd = false;
Expand Down
6 changes: 3 additions & 3 deletions FMB/FiniteModelMultiSorted.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,10 +45,10 @@ class FiniteModelMultiSorted {
// Assume def is an equality literal with a
// function application on lhs and constant on rhs
void addConstantDefinition(unsigned f, unsigned res);
void addFunctionDefinition(unsigned f, const DArray<unsigned>& args, unsigned res);
void addFunctionDefinition(unsigned f, const DArray<unsigned>& args, unsigned res);
// Assume def is non-equality ground literal
void addPropositionalDefinition(unsigned f, bool res);
void addPredicateDefinition(unsigned f, const DArray<unsigned>& args, bool res);
void addPredicateDefinition(unsigned f, const DArray<unsigned>& args, bool res);

bool isPartial();

Expand Down Expand Up @@ -87,7 +87,7 @@ class FiniteModelMultiSorted {
std::pair<unsigned,unsigned> pair = std::make_pair(c,srt);
if(_domainConstants.find(pair,t)) return t;
std::string name = "domCon_"+env.signature->typeConName(srt)+"_"+Lib::Int::toString(c);
unsigned f = env.signature->addFreshFunction(0,name.c_str());
unsigned f = env.signature->addFreshFunction(0,name.c_str());
TermList srtT = TermList(AtomicSort::createConstant(srt));
env.signature->getFunction(f)->setType(OperatorType::getConstantsType(srtT));
t = Term::createConstant(f);
Expand Down
44 changes: 29 additions & 15 deletions FMB/Monotonicity.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,8 +50,8 @@ Monotonicity::Monotonicity(ClauseList* clauses, unsigned srt) : _srt(srt)
_pF.insert(p,SATLiteral(_solver->newVar(),true));

Stack<SATLiteral> slits;
slits.push(_pT.get(p).opposite());
slits.push(_pF.get(p).opposite());
slits.push(_pT.get(p).opposite());
slits.push(_pF.get(p).opposite());
_solver->addClause(SATClause::fromStack(slits));
}

Expand All @@ -68,13 +68,27 @@ Monotonicity::Monotonicity(ClauseList* clauses, unsigned srt) : _srt(srt)
_result = (status == SATSolver::Status::SATISFIABLE);
}

DArray<signed char>* Monotonicity::check() {
if (!_result) return nullptr;

DArray<signed char>* res = new DArray<signed char>(env.signature->predicates());
(*res)[0] = 0; // pick a value for the 0-th = predicate (we don't really care here)
for(unsigned p=1;p<env.signature->predicates();p++){
bool trueExt = _solver->getAssignment(_pT.get(p).var());
bool falseExt = _solver->getAssignment(_pF.get(p).var());
ASS(!trueExt || !falseExt)
(*res)[p] = trueExt ? 1 : (falseExt ? -1 : 0);
}

return res;
}

void Monotonicity::monotone(Clause* c, Literal* l)
{
// if we have equality
if(l->isEquality()){
TermList* t1 = l->nthArgument(0);
TermList* t2 = l->nthArgument(1);
TermList* t1 = l->nthArgument(0);
TermList* t2 = l->nthArgument(1);
// t1 = t2
if(l->polarity()){
// add a clause for each
Expand Down Expand Up @@ -134,12 +148,12 @@ bool Monotonicity::guards(Literal* l, unsigned var, Stack<SATLiteral>& slits)
if(!l->polarity()){
TermList* t1 = l->nthArgument(0);
TermList* t2 = l->nthArgument(1);
if(t1->isVar() && t1->var()==var) return true;
if(t2->isVar() && t2->var()==var) return true;
if(t1->isVar() && t1->var()==var) return true;
if(t2->isVar() && t2->var()==var) return true;
}
}
else{
// check if l contains X
// check if l contains X
unsigned p = l->functor();
for(unsigned i=0;i<l->arity();i++){
TermList* t = l->nthArgument(i);
Expand Down Expand Up @@ -189,7 +203,7 @@ void Monotonicity::addSortPredicates(bool withMon, ClauseList*& clauses, const D

// Now add the relevant axioms for these new sort predicates i.e.
// 1) ?[X] : p(X) (need skolem constant) = p(sk)
// 2) for each function f with return sort s
// 2) for each function f with return sort s
// !args : p(f(args))
unsigned function_count = env.signature->functions();
for(unsigned s=0;s<env.signature->typeCons();s++){
Expand All @@ -209,14 +223,14 @@ void Monotonicity::addSortPredicates(bool withMon, ClauseList*& clauses, const D
unsigned arity = env.signature->functionArity(f);
static Stack<TermList> vars;
vars.reset();
for(unsigned x=0;x<arity;x++) vars.push(TermList(x,false));
for(unsigned x=0;x<arity;x++) vars.push(TermList(x,false));

Term* fX = Term::create(f,arity,vars.begin());
Literal* pfX = Literal::create1(p,true,TermList(fX));
auto fINs = Clause::fromLiterals({ pfX }, NonspecificInference0(UnitInputType::AXIOM,InferenceRule::INPUT));
ClauseList::push(fINs,newAxioms);
ASS(SortHelper::areSortsValid(fINs));
}
}

// Next the non-empty constraint
unsigned skolemConstant = env.signature->addSkolemFunction(0);
Expand All @@ -242,7 +256,7 @@ void Monotonicity::addSortPredicates(bool withMon, ClauseList*& clauses, const D
sortedVariables.reset();

DHMap<unsigned,TermList> varSorts;
SortHelper::collectVariableSorts(cl,varSorts);
SortHelper::collectVariableSorts(cl,varSorts);
for(unsigned v=0;v<cl->varCnt();v++){
TermList vsrt;
if(varSorts.find(v,vsrt)){
Expand All @@ -251,11 +265,11 @@ void Monotonicity::addSortPredicates(bool withMon, ClauseList*& clauses, const D
}
// else the var isn't used in the clause...they're not normalised
}

if(!sortedVariables.isEmpty()){

Stack<Literal*> literals;
literals.loadFromIterator(cl->iterLits());
Stack<Literal*> literals;
literals.loadFromIterator(cl->iterLits());

Stack<std::pair<unsigned,unsigned>>::Iterator vit(sortedVariables);
while(vit.hasNext()){
Expand All @@ -277,7 +291,7 @@ void Monotonicity::addSortPredicates(bool withMon, ClauseList*& clauses, const D
//cout << "REPLACING" << endl;
//cout << cl->toString() << endl;
//cout << replacement->toString() << endl;
it.del();
it.del();
}
}

Expand Down
Loading

0 comments on commit 4768334

Please sign in to comment.