/*****************************************************************************/
/*!
* \file theory_quant.cpp
*
* Author: Daniel Wichs, Yeting Ge
*
* Created: Wednesday July 2, 2003
*
* <hr>
*
* License to use, copy, modify, sell and/or distribute this software
* and its documentation for any purpose is hereby granted without
* royalty, subject to the terms and conditions defined in the \ref
* LICENSE file provided with this distribution.
*
* <hr>
*
*/
/*****************************************************************************/
#include "theory_quant.h"
#include "theory_arith.h"
#include "theory_array.h"
#include "typecheck_exception.h"
#include "parser_exception.h"
#include "smtlib_exception.h"
#include "quant_proof_rules.h"
#include "theory_core.h"
#include "command_line_flags.h"
#include "vcl.h"
#include<string>
#include<string.h>
#include <algorithm>
using namespace std;
using namespace CVC3;
///////////////////////////////////////////////////////////////////////////////
// TheoryQuant Public Methods //
///////////////////////////////////////////////////////////////////////////////
static const Expr null_expr;
const int FOUND_FALSE = 1;
Trigger::Trigger(TheoryCore* core, Expr e, Polarity pol, std::set<Expr> boundVars){
trig=e ;
polarity=pol;
head=null_expr;
hasRWOp=false;
hasTrans=false;
hasT2=false;
isSimple=false;
isSuperSimple=false;
isMulti=false;
multiIndex = 99999;
multiId = 99999;
for(std::set<Expr>::const_iterator i=boundVars.begin(),iend=boundVars.end(); i!=iend; ++i)
bvs.push_back(*i);
}
bool Trigger::isPos(){
return (Pos==polarity||PosNeg==polarity);
}
bool Trigger::isNeg(){
return (Neg==polarity || PosNeg==polarity);
}
std::vector<Expr> Trigger::getBVs(){
return bvs;
}
Expr Trigger::getEx(){
return trig;
}
void Trigger::setHead(Expr h){
head=h;
}
Expr Trigger::getHead(){
return head;
}
void Trigger::setRWOp(bool b){
hasRWOp =b ;
}
bool Trigger::hasRW(){
return hasRWOp;
}
void Trigger::setTrans(bool b){
hasTrans =b ;
}
bool Trigger::hasTr(){
return hasTrans;
}
void Trigger::setTrans2(bool b){
hasT2 =b ;
}
bool Trigger::hasTr2(){
return hasT2;
}
void Trigger::setSimp(){
isSimple =true ;
}
bool Trigger::isSimp(){
return isSimple;
}
void Trigger::setSuperSimp(){
isSuperSimple =true ;
}
bool Trigger::isSuperSimp(){
return isSuperSimple;
}
void Trigger::setMultiTrig(){
isMulti = true ;
}
bool Trigger::isMultiTrig(){
return isMulti;
}
dynTrig::dynTrig(Trigger t, ExprMap<Expr> b, size_t id)
:trig(t),
univ_id(id),
binds(b)
{}
TheoryQuant::TheoryQuant(TheoryCore* core) //!< Constructor
: Theory(core, "Quantified Expressions"),
d_univs(core->getCM()->getCurrentContext()),
d_rawUnivs(core->getCM()->getCurrentContext()),
d_arrayTrigs(core->getCM()->getCurrentContext()),
d_lastArrayPos(core->getCM()->getCurrentContext(), 0 , 0),
d_lastPredsPos(core->getCM()->getCurrentContext(), 0, 0),
d_lastTermsPos(core->getCM()->getCurrentContext(), 0, 0),
d_lastPartPredsPos(core->getCM()->getCurrentContext(), 0, 0),
d_lastPartTermsPos(core->getCM()->getCurrentContext(), 0, 0),
d_univsPartSavedPos(core->getCM()->getCurrentContext(), 0, 0),
d_lastPartLevel(core->getCM()->getCurrentContext(), 0, 0),
d_usefulGterms(core->getCM()->getCurrentContext()),
d_lastUsefulGtermsPos(core->getCM()->getCurrentContext(), 0, 0),
d_savedTermsPos(core->getCM()->getCurrentContext(), 0, 0),
d_univsSavedPos(core->getCM()->getCurrentContext(), 0, 0),
d_rawUnivsSavedPos(core->getCM()->getCurrentContext(), 0, 0),
d_univsPosFull(core->getCM()->getCurrentContext(), 0, 0),
d_univsContextPos(core->getCM()->getCurrentContext(), 0, 0),
d_instCount(core->getCM()->getCurrentContext(), 0,0),
d_contextTerms(core->getCM()->getCurrentContext()),
d_contextCache(core->getCM()->getCurrentContext()),
d_maxQuantInst(&(core->getFlags()["max-quant-inst"].getInt())),
d_useNew(&(core->getFlags()["quant-new"].getBool())),
d_useLazyInst(&(core->getFlags()["quant-lazy"].getBool())),
d_useSemMatch(&(core->getFlags()["quant-sem-match"].getBool())),
d_useAtomSem(&(core->getFlags()["quant-const-match"].getBool())),
d_translate(&(core->getFlags()["translate"].getBool())),
d_useTrigNew(&(core->getFlags()["quant-trig-new"].getBool())),
d_usePart(&(core->getFlags()["quant-inst-part"].getBool())),
d_useMult(&(core->getFlags()["quant-inst-mult"].getBool())),
d_useInstEnd(&(core->getFlags()["quant-inst-end"].getBool())),
d_useInstLCache(&(core->getFlags()["quant-inst-lcache"].getBool())),
d_useInstGCache(&(core->getFlags()["quant-inst-gcache"].getBool())),
d_useInstTrue(&(core->getFlags()["quant-inst-true"].getBool())),
d_usePullVar(&(core->getFlags()["quant-pullvar"].getBool())),
d_useExprScore(&(core->getFlags()["quant-score"].getBool())),
d_useTrigLoop(&(core->getFlags()["quant-trig-loop"].getInt())),
d_maxInst(&(core->getFlags()["quant-max-inst"].getInt())),
d_useTrans(&(core->getFlags()["quant-trans3"].getBool())),
d_useTrans2(&(core->getFlags()["quant-trans2"].getBool())),
d_useInstAll(&(core->getFlags()["quant-inst-all"].getBool())),
d_usePolarity(&(core->getFlags()["quant-polarity"].getBool())),
d_useEqu(&(core->getFlags()["quant-equ"].getBool())),
d_maxNaiveCall(&(core->getFlags()["quant-naive-num"].getInt())),
d_curMaxExprScore(core->getCM()->getCurrentContext(), (core->getFlags()["quant-max-score"].getInt()),0),
d_arrayIndic(core->getCM()->getCurrentContext()),
d_exprLastUpdatedPos(core->getCM()->getCurrentContext(),0 ,0),
d_trans_found(core->getCM()->getCurrentContext()),
d_trans2_found(core->getCM()->getCurrentContext()),
null_cdlist(core->getCM()->getCurrentContext()),
d_eqs(core->getCM()->getCurrentContext()),
d_eqs_pos(core->getCM()->getCurrentContext(), 0, 0),
d_allInstCount(core->getStatistics().counter("quantifier instantiations")),
d_partCalled(core->getCM()->getCurrentContext(),false,0),
d_instHistory(core->getCM()->getCurrentContext()),
d_alltrig_list(core->getCM()->getCurrentContext())
{
IF_DEBUG(d_univs.setName("CDList[TheoryQuant::d_univs]"));
vector<int> kinds;
d_instCount = 0;
d_cacheThmPos=0;
d_trans_num=0;
d_trans2_num=0;
d_rules=createProofRules();
kinds.push_back(EXISTS);
kinds.push_back(FORALL);
registerTheory(this, kinds);
d_partCalled=false;
d_offset_multi_trig=2;
d_initMaxScore=(theoryCore()->getFlags()["quant-max-score"].getInt());
for(size_t i=0; i<MAX_TRIG_BVS; i++){
d_mybvs[i] = getEM()->newBoundVarExpr("_genbv", int2string(i), Type::anyType(getEM()));
}
}
//! Destructor
TheoryQuant::~TheoryQuant() {
if(d_rules != NULL) delete d_rules;
for(std::map<Type, CDList<size_t>* ,TypeComp>::iterator
it = d_contextMap.begin(), iend = d_contextMap.end();
it!= iend; ++it) {
delete it->second;
free(it->second);
}
}
int TheoryQuant::getExprScore(const Expr& e){
return theoryCore()->getQuantLevelForTerm(e);
}
bool isSysPred(const Expr& e){
return ( isLE(e) || isLT(e) || isGE(e) || isGT(e) || e.isEq());
}
bool canGetHead(const Expr& e){
return (e.getKind() == APPLY || e.getKind() == READ || e.getKind() == WRITE);
}
bool isSimpleTrig(const Expr& t){
if(!canGetHead(t)) return false;
for(int i = 0; i < t.arity(); i++){
if (t[i].arity()>0 && t[i].containsBoundVar()) return false;
if (BOUND_VAR == t[i].getKind()){
for(int j = 0; j < i; j++){
if(t[i] == t[j]) return false;
}
}
}
return true;
}
bool isSuperSimpleTrig(const Expr& t){
if(!isSimpleTrig(t)) return false;
for(int i = 0; i < t.arity(); i++){
if (t[i].arity()>0 ) return false;
if (BOUND_VAR != t[i].getKind()){
return false;
}
}
return true;
}
bool usefulInMatch(const Expr& e){
if(e.arity() == 0){
TRACE("usefulInMatch", e.toString()+": ",e.arity(), "");
TRACE("usefulInMatch", e.isRational(), "", "");
}
return ( canGetHead(e) || (isSysPred(e) && (!e.isEq()) ) );
}
void TheoryQuant::setup(const Expr& e) {}
void TheoryQuant::update(const Theorem& t, const Expr& e) {
}
std::string vectorExpr2string(const std::vector<Expr> & vec){
std::string buf;
for(size_t i=0; i<vec.size(); i++){
buf.append(vec[i].toString());
buf.append(" # ");
}
return buf;
}
static void recursiveGetSubTrig(const Expr& e, std::vector<Expr> & res) {
if(e.getFlag())
return;
if(e.isClosure())
return recursiveGetSubTrig(e.getBody(),res);
if (e.isApply()|| isSysPred(e)){
res.push_back(e);
}
else
if ( e.isTerm() && (!e.isVar()) && (e.getKind()!=RATIONAL_EXPR) ) {
res.push_back(e);
}
for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
recursiveGetSubTrig(*i,res);
}
e.setFlag();
return ;
}
std::vector<Expr> getSubTrig(const Expr& e){
e.clearFlags();
std::vector<Expr> res;
recursiveGetSubTrig(e,res);
e.clearFlags();
TRACE("getsub","e is ", e.toString(),"");
TRACE("getsub","have ", res.size()," subterms");
return res;
}
static void recGetSubTerms(const Expr& e, std::vector<Expr> & res) {
if(e.getFlag())
return;
if(e.isClosure())
return recGetSubTerms(e.getBody(),res);
for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
recGetSubTerms(*i,res);
}
res.push_back(e);
e.setFlag();
return ;
}
const std::vector<Expr>& TheoryQuant::getSubTerms(const Expr& e){
//the last item in res is e itself
ExprMap<std::vector<Expr> >::iterator iter= d_subTermsMap.find(e);
if( d_subTermsMap.end() == iter){
e.clearFlags();
std::vector<Expr> res;
recGetSubTerms(e,res);
e.clearFlags();
TRACE("getsubs", "getsubs, e is: ", e, "");
TRACE("getsubs", "e has ", res.size(), " subterms");
d_subTermsMap[e] = res;
return d_subTermsMap[e];
}
else{
return (*iter).second;
}
}
void TheoryQuant::enqueueInst(const Theorem& univ, const vector<Expr>& bind, const Expr& gterm){
static int max_score =-1;
bool partInst=false;
if(bind.size() < univ.getExpr().getVars().size()){
partInst=false;
TRACE("sendinst","partinst",partInst,"");
}
Expr bind_expr(RAW_LIST, bind, getEM());
if (*d_useInstLCache){
const Expr& e = univ.getExpr();
ExprMap<CDMap<Expr,bool>*>::iterator iterCache = d_bindHistory.find(e);
if (iterCache != d_bindHistory.end()){
CDMap<Expr,bool>* cache = (*iterCache).second;
if(cache->find(bind_expr) !=cache->end()){
return ;
}
else{
(*cache)[bind_expr] = true;
}
}
else{
CDMap<Expr,bool>* new_cache = new(true) CDMap<Expr,bool> (theoryCore()->getCM()->getCurrentContext());
(*new_cache)[bind_expr] = true;
}
}
Theorem thm ;
if(null_expr == gterm ){//it is from naive instantiation or multi-inst
TRACE("sendinst","gterm",gterm,"");
if(partInst) {
thm = d_rules->partialUniversalInst(univ, bind, 0);
}
else{
thm = d_rules->universalInst(univ, bind, 0);
}
}
else{
int gscore = theoryCore()->getQuantLevelForTerm(gterm);
if(gscore > max_score){
max_score = gscore;
// cout<<"max score "<<max_score<<endl;
}
if(partInst) {
thm = d_rules->partialUniversalInst(univ, bind, gscore);
}
else{
thm = d_rules->universalInst(univ, bind, gscore);
}
}
Theorem simpThm = simplify(thm.getExpr());
if(*d_useInstTrue){
Expr res = simpThm.getRHS();
if(res.isTrue()){
return;
}
if(res.isFalse() ){
enqueueFact(thm);
// setInconsistent(simpThm);
d_allInstCount++;
d_instThisRound++;
throw FOUND_FALSE;
}
}
d_simplifiedThmQueue.push(thm);
TRACE("quant sendinst", "=gterm: ",gterm, "");
TRACE("quant sendinst", "==add fact simp =", simplifyExpr(thm.getExpr()), "");
TRACE("quant sendinst", "==add fact org =", thm.getExpr(), "");
TRACE("quant sendinst", "==add fact from= ", univ.getExpr(), "\n===: "+vectorExpr2string(bind));
}
void TheoryQuant::enqueueInst(size_t univ_id , const std::vector<Expr>& bind, const Expr& gterm){
static int max_score =-1;
const Theorem& univ = d_univs[univ_id];
bool partInst=false;
if(bind.size() < univ.getExpr().getVars().size()){
partInst=false;
TRACE("sendinst","partinst",partInst,"");
}
Expr bind_expr(RAW_LIST, bind, getEM());
if (*d_useInstLCache){
const Expr& e = univ.getExpr();
ExprMap<CDMap<Expr,bool>*>::iterator iterCache = d_bindHistory.find(e);
if (iterCache != d_bindHistory.end()){
CDMap<Expr,bool>* cache = (*iterCache).second;
if(cache->find(bind_expr) !=cache->end()){
return ;
}
else{
(*cache)[bind_expr] = true;
}
}
else{
CDMap<Expr,bool>* new_cache = new(true) CDMap<Expr,bool> (theoryCore()->getCM()->getCurrentContext());
(*new_cache)[bind_expr] = true;
}
}
Theorem thm ;
if(null_expr == gterm ){//it is from naive instantiation or multi-inst
TRACE("sendinst","gterm",gterm,"");
if(partInst) {
thm = d_rules->partialUniversalInst(univ, bind, 0);
}
else{
thm = d_rules->universalInst(univ, bind, 0);
}
}
else{
int gscore = theoryCore()->getQuantLevelForTerm(gterm);
if(gscore > max_score){
max_score = gscore;
// cout<<"max score "<<max_score<<endl;
}
if(partInst) {
thm = d_rules->partialUniversalInst(univ, bind, gscore);
}
else{
thm = d_rules->universalInst(univ, bind, gscore);
}
}
Theorem simpThm = simplify(thm.getExpr());
if(*d_useInstTrue){
Expr res = simpThm.getRHS();
if(res.isTrue()){
return;
}
if(res.isFalse() ){
enqueueFact(thm);
// setInconsistent(simpThm);
d_allInstCount++;
d_instThisRound++;
throw FOUND_FALSE;
}
}
d_simplifiedThmQueue.push(thm);
// cout<<"enqueue inst"<<thm << endl;
TRACE("quant sendinst", "=gterm: ",gterm, "");
TRACE("quant sendinst", "==add fact simp =", simplifyExpr(thm.getExpr()), "");
TRACE("quant sendinst", "==add fact org =", thm.getExpr(), "");
TRACE("quant sendinst", "==add fact from= ", univ.getExpr(), "\n===: "+vectorExpr2string(bind));
}
void TheoryQuant::enqueueInst(const Theorem& univ,
Trigger& trig,
const std::vector<Expr>& binds,
const Expr& gterm
) {
return enqueueInst(univ,binds,gterm);
}
int TheoryQuant::sendInstNew(){
int resNum = 0 ;
while(!d_simplifiedThmQueue.empty()){
const Theorem thm = d_simplifiedThmQueue.front();
d_simplifiedThmQueue.pop();
d_allInstCount++;
d_instThisRound++;
resNum++;
enqueueFact(thm);
}
return resNum;
}
void TheoryQuant::addNotify(const Expr& e){}
int recursiveExprScore(const Expr& e) {
int res=0;
DebugAssert(!(e.isClosure()), "exprScore called on closure");
if(e.arity()== 0){
res = 0;
}
else{
for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
res += recursiveExprScore(*i);
}
}
res++;
return res;
}
int exprScore(const Expr& e){
return recursiveExprScore(e);
}
Expr getHeadExpr(const Expr& e){
if (e.getKind() == APPLY){
return e.getOp().getExpr();
}
if ( READ == e.getKind() || WRITE == e.getKind() ) {
int kind = e[0].getKind();
if (UCONST==kind) {
return e[0];
}
else if (APPLY==kind || UFUNC == kind || READ == kind || WRITE == kind){
return getHeadExpr(e[0]);
}
else if(e[0].isSkolem()){
return e[0];
}
}
return null_expr;
}
Expr getHead(const Expr& e) {
return getHeadExpr(e);
}
//! get the bound vars in term e,
static bool recursiveGetBoundVars(const Expr& e, std::set<Expr>& result) {
bool res(false);
if(e.getFlag()){
return e.containsBoundVar();
}
else if(e.isClosure()){
res = recursiveGetBoundVars(e.getBody(),result);
}
else if (BOUND_VAR == e.getKind() ){
result.insert(e);
e.setContainsBoundVar();
res = true;
}
else {
res = false;
for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i){
if(recursiveGetBoundVars(*i,result)){
res = true;
}
}
}
e.setFlag();
if(res) {
e.setContainsBoundVar();
}
return res;
}
//! get bound vars in term e,
std::set<Expr> getBoundVars(const Expr& e){
/*
// static ExprMap<std::set<Expr> > bvsCache;
static std::map<Expr, std::set<Expr> > bvsCache;
std::map<Expr, std::set<Expr> >::iterator iterCache = bvsCache.find(e);
//ExprMap<std::set<Expr> >::iterator iterCache = bvsCache.find(e);
if (iterCache != bvsCache.end()){
// return iterCache->second;
return (*iterCache).second;
}
*/
e.clearFlags();
std::set<Expr> result ;
recursiveGetBoundVars(e,result);
e.clearFlags();
// bvsCache[e]=result;
return result;
}
bool isGoodSysPredTrigger(const Expr& e){
if(!isSysPred(e)) return false;
if(usefulInMatch(e[0]) || usefulInMatch(e[1])) return true;
return false;
}
bool isGoodFullTrigger(const Expr& e, const std::vector<Expr>& bVarsThm){
if( !usefulInMatch(e))
return false;
const std::set<Expr>& bvs = getBoundVars(e);
if (bvs.size() >= bVarsThm.size()){
for(size_t i=0; i<bVarsThm.size(); i++) {
if (bvs.find(bVarsThm[i]) == bvs.end()){
return false;
}
}
return true;
}
else {
return false;
}
}
bool isGoodMultiTrigger(const Expr& e, const std::vector<Expr>& bVarsThm, int offset){
if( !usefulInMatch(e) )
return false;
int bvar_missing = 0;
const std::set<Expr>& bvs = getBoundVars(e);
if(bvs.size() <= 0) return false;
for(size_t i=0; i<bVarsThm.size(); i++) {
if (bvs.find(bVarsThm[i]) == bvs.end()){
bvar_missing++; // found one bound var missing in the e.
}
}
if (0 == bvar_missing){ //it is a full triggers
return false;
}
if(bvar_missing <= offset){
if(isSysPred(e)){
if (isGoodSysPredTrigger(e)) {
return true;
}
else {
return false;
}
}
else {
return true;
}
}
return false;
}
bool isGoodPartTrigger(const Expr& e, const std::vector<Expr>& bVarsThm){
if( !usefulInMatch(e) )
return false;
size_t bvar_missing = 0;
const std::set<Expr>& bvs = getBoundVars(e);
for(size_t i=0; i<bVarsThm.size(); i++) {
if (bvs.find(bVarsThm[i]) == bvs.end()){
bvar_missing++; // found one bound var missing in the e.
}
}
if (0 == bvar_missing){ //it is a full triggers
return false;
}
if(0 == bvs.size()){
return false;
}
if(bvar_missing < bVarsThm.size()){
if(isSysPred(e)){
if (isGoodSysPredTrigger(e)) {
return true;
}
else {
return false;
}
}
else {
return true;
}
}
return false;
}
static bool recursiveGetPartTriggers(const Expr& e, std::vector<Expr>& res) {
if(e.getFlag())
return false;
if(e.isClosure())
return recursiveGetPartTriggers(e.getBody(), res);
if(0 == e.arity()){
if(BOUND_VAR == e.getKind()){
return false;
}
else{
return true;
}
}
bool good=true;
bool no_bound =true;
for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
if(BOUND_VAR == i->getKind()){
no_bound=false;
continue;
}
bool temp = recursiveGetPartTriggers(*i,res);
if(false == temp) {
good=false;
}
}
e.setFlag();
if(good && no_bound) {
return true;
}
else if(good && !no_bound){
res.push_back(e);
return false;
}
else{
return false;
}
}
std::vector<Expr> getPartTriggers(const Expr& e){
e.clearFlags();
std::vector<Expr> res;
recursiveGetPartTriggers(e,res);
e.clearFlags();
return res;
}
int trigInitScore(const Expr& e){
if( isSysPred(e) && !isGoodSysPredTrigger(e)){
return 1;
}
else {
return 0;
}
}
void findPolarity(const Expr& e, ExprMap<Polarity>& res, Polarity pol){
if(!e.getType().isBool()) return;
//now a AND b will be given a polarity too, this is not necessary.
if(res.count(e)>0){
if ((Neg == res[e] && Pos == pol) || (Neg == res[e] && Pos == pol) ){
res[e]=PosNeg;
}
}
else{
res[e]=pol;
}
if(PosNeg==pol){
for(int i=0; i<e.arity(); i++){
findPolarity(e[i], res, pol);
}
}
else{
Polarity neg_pol=Ukn;
if(Pos == pol) {
neg_pol = Neg;
}
else if(Neg == pol){
neg_pol = Pos;
}
if(e.isImpl()){
findPolarity(e[0], res, neg_pol);
findPolarity(e[1], res, pol);
}
else if(e.isAnd() || e.isOr()){
for(int i=0; i<e.arity(); i++){
findPolarity(e[i], res, pol);
}
}
else if(e.isNot()){
findPolarity(e[0], res, neg_pol);
}
else if(e.isITE()){
findPolarity(e[0], res, PosNeg);
findPolarity(e[1], res, pol);
findPolarity(e[2], res, pol);
}
else if(e.isClosure()){
findPolarity(e.getBody(), res, pol);
}
else if(e.isIff()){
findPolarity(e[0], res, PosNeg);
findPolarity(e[1], res, PosNeg);
}
else if(e.isXor()){
findPolarity(e[0], res, neg_pol);
findPolarity(e[1], res, neg_pol);
}
else if(e.isAtomicFormula()){
return;
}
else{
DebugAssert(false, "Error in find polarity in "+e.toString());
}
}
}
void TheoryQuant::arrayIndexName(const Expr& e){
std::vector<Expr> res;
const std::vector<Expr>& subs=getSubTerms(e);
for(size_t i=0; i<subs.size(); i++){
int kind = subs[i].getKind();
if (READ == kind || WRITE == kind){
const Expr& name = subs[i][0];
const Expr& index = subs[i][1];
if(getBoundVars(name).size() <= 0 && (getBoundVars(index).size() <=0)){
std::vector<Expr> tp = d_arrayIndic[name];
tp.push_back(index);
d_arrayIndic[name]=tp;
}
else {
}
}
}
}
void TheoryQuant::registerTrig(ExprMap<ExprMap<std::vector<dynTrig>* >* >& cur_trig_map,
Trigger trig,
const std::vector<Expr> thmBVs,
size_t univ_id){
{
if(trig.hasRWOp){
ExprMap<Expr> bv_map;
dynTrig newDynTrig(trig, bv_map,univ_id);
d_arrayTrigs.push_back(newDynTrig);
}
}
ExprMap<Expr> bv_map;
for(size_t i = 0; i<thmBVs.size(); i++){
bv_map[thmBVs[i]] = null_expr;
}
const Expr& trig_ex = trig.getEx();
Expr genTrig = generalTrig(trig_ex, bv_map);
dynTrig newDynTrig(trig,bv_map,univ_id);
Expr head = trig.getHead();
ExprMap<ExprMap<vector<dynTrig>* >* >::iterator iter = cur_trig_map.find(head);
if(cur_trig_map.end() == iter){
ExprMap<vector<dynTrig>* >* new_cd_map= new ExprMap<vector<dynTrig>* > ;
cur_trig_map[head] = new_cd_map;
vector<dynTrig>* new_dyntrig_list = new vector<dynTrig>;
(*new_cd_map)[genTrig] = new_dyntrig_list;
(*new_dyntrig_list).push_back(newDynTrig);
}
else{
ExprMap<vector<dynTrig>* >* cd_map = iter->second;
ExprMap<vector<dynTrig>* >::iterator iter_map = cd_map->find(genTrig);
if(cd_map->end() == iter_map){
vector<dynTrig>* new_dyntrig_list = new vector<dynTrig>;
(*cd_map)[genTrig] = new_dyntrig_list;
(*new_dyntrig_list).push_back(newDynTrig);
}
else{
// (*((*cd_map)[generalTrig])).push_back(newDynTrig);
(*(iter_map->second)).push_back(newDynTrig);
}
}
}
/*
void TheoryQuant::registerTrigReal(Trigger trig, const std::vector<Expr> thmBVs, size_t univ_id){
cout<<"register: "<<trig.getEx()<<endl;
ExprMap<Expr> bv_map;
for(size_t i = 0; i<thmBVs.size(); i++){
bv_map[thmBVs[i]] = null_expr;
}
const Expr& trig_ex = trig.getEx();
Expr genTrig = generalTrig(trig_ex, bv_map);
dynTrig newDynTrig(trig,bv_map,univ_id);
Expr head = trig.getHead();
ExprMap<CDMap<Expr, CDList<dynTrig>* >* >::iterator iter = d_allmap_trigs.find(head);
if(d_allmap_trigs.end() == iter){
CDMap<Expr, CDList<dynTrig>* >* new_cd_map=
new(true) CDMap<Expr, CDList<dynTrig>* > (theoryCore()->getCM()->getCurrentContext());
d_allmap_trigs[head] = new_cd_map;
CDList<dynTrig>* new_dyntrig_list = new(true) CDList<dynTrig> (theoryCore()->getCM()->getCurrentContext());
(*new_cd_map)[genTrig] = new_dyntrig_list;
(*new_dyntrig_list).push_back(newDynTrig);
}
else{
CDMap<Expr, CDList<dynTrig>* >* cd_map = iter->second;
CDMap<Expr, CDList<dynTrig>* >::iterator iter_map = cd_map->find(genTrig);
if(cd_map->end() == iter_map){
CDList<dynTrig>* new_dyntrig_list = new(true) CDList<dynTrig> (theoryCore()->getCM()->getCurrentContext());
(*cd_map)[genTrig] = new_dyntrig_list;
(*new_dyntrig_list).push_back(newDynTrig);
}
else{
// (*((*cd_map)[generalTrig])).push_back(newDynTrig);
(*((*iter_map).second)).push_back(newDynTrig);
cout<<"once more"<<endl;
}
}
}
*/
Expr TheoryQuant::generalTrig(const Expr& trig, ExprMap<Expr>& bvs){
size_t count =1 ;
Expr res = recGeneralTrig(trig, bvs, count);
getBoundVars(res);
return res;
}
Expr TheoryQuant::recGeneralTrig(const Expr& trig, ExprMap<Expr>& bvs, size_t& mybvs_count){
if (!trig.containsBoundVar()) return trig;
if (BOUND_VAR == trig.getKind()){
if (bvs.find(trig) != bvs.end()){
const Expr& ubv = bvs[trig];
if(null_expr ==ubv){
Expr new_bv = d_mybvs[mybvs_count++];
bvs[trig] = new_bv ;
if((mybvs_count) >= MAX_TRIG_BVS ){
throw "general trig error";
}
else{
return new_bv;
}
}
else{
return bvs[trig];
}
}
else{
return d_mybvs[0];
}
}
else{
vector<Expr> children;
for(Expr::iterator i=trig.begin(), iend=trig.end(); i!=iend; ++i){
Expr repChild;
if(i->containsBoundVar()){
repChild = recGeneralTrig(*i, bvs, mybvs_count);
}
else{
repChild = *i;
}
children.push_back(repChild);
}
return Expr(trig.getOp(), children);
}
}
//this function is used to check if two triggers can match with eath other
bool TheoryQuant::canMatch(const Expr& t1, const Expr& t2, ExprMap<Expr>& env){
if(getBaseType(t1) != getBaseType(t2)) return false;
if (BOUND_VAR == t1.getKind() || BOUND_VAR == t2.getKind()) {
return true;
}
if ( (t1.arity() != t2.arity()) || (t1.getKind() != t2.getKind() )) {
return false;
}
if (canGetHead(t1) && canGetHead(t2)) {
if ( getHead(t1) != getHead(t2) ){
return false;
}
for(int i=0; i<t1.arity(); i++){
if (false == canMatch(t1[i], t2[i] , env))
return false;
}
return true;
}
else{
return false;
}
}
bool TheoryQuant::isTransLike (const vector<Expr>& cur_trig){
if(!(*d_useTrans)){
return false;
}
if(3==cur_trig.size()){
const Expr& t1=cur_trig[0];
const Expr& t2=cur_trig[1];
const Expr& t3=cur_trig[2];
if ( canGetHead(t1) && canGetHead(t2) && canGetHead(t3) &&
(getHead(t1) == getHead(t2)) && (getHead(t2) == getHead(t3))){
const std::set<Expr>& ts1 = getBoundVars(t1);
const std::set<Expr>& ts2 = getBoundVars(t2);
const std::set<Expr>& ts3 = getBoundVars(t3);
if ( 2==ts1.size() && 2==ts2.size() && 2==ts2.size() &&
(ts1 != ts2) && (ts2 != ts3) && (ts3 != ts1)){
std::set<Expr> all;
for(set<Expr>::const_iterator i=ts1.begin(), iend = ts1.end(); i != iend; i++){
all.insert(*i);
}
for(set<Expr>::const_iterator i=ts2.begin(), iend = ts2.end(); i != iend; i++){
all.insert(*i);
}
for(set<Expr>::const_iterator i=ts3.begin(), iend = ts3.end(); i != iend; i++){
all.insert(*i);
}
bool res = true;
if(3==all.size()){
for(set<Expr>::const_iterator i=all.begin(), iend = all.end(); i != iend; i++){
if(!i->isVar()) {
res = false;
break;
}
}
if(res) {
}
return res;
}
}
}
}
return false;
}
bool TheoryQuant::isTrans2Like (const std::vector<Expr>& all_terms, const Expr& tr2){
if(!(*d_useTrans2)){
return false;
}
for(size_t i = 0; i < all_terms.size(); i++){
if(all_terms[i].isEq()){
const Expr& cur = all_terms[i];
if(cur[0] != cur[1] && ( (cur[0]==tr2[0] && cur[1]==tr2[1]) || (cur[0]==tr2[1] && cur[1]==tr2[0]))){
return true;
}
}
}
return false;
}
bool goodMultiTriggers(const std::vector<Expr>& exprs, const std::vector<Expr> bVars){
ExprMap<bool> bvar_found;
for( std::vector<Expr>::const_iterator i = bVars.begin(), iend= bVars.end(); i!=iend; i++) {
bvar_found[*i]=false;
}
for (size_t i=0; i< exprs.size();i++){
const std::set<Expr> & bv_in_trig = getBoundVars(exprs[i]);
for(std::set<Expr>::const_iterator j=bv_in_trig.begin(), jend = bv_in_trig.end(); j != jend; j++){
if(bvar_found.find(*j) != bvar_found.end()){
bvar_found[*j]=true;
}
}
}
for( std::vector<Expr>::const_iterator i = bVars.begin(), iend= bVars.end(); i!=iend; i++) {
if(false == bvar_found[*i]){
return false ;
}
}
return true;
}
inline size_t locVar(const vector<Expr>& bvsThm, const Expr& bv){
for(size_t i=0, iend = bvsThm.size(); i < iend; i++){
if (bvsThm[i] == bv){
return i;
}
}
return 999; //this number should be big enough
}
void TheoryQuant::setupTriggers(const Theorem& thm, size_t univs_id){
}
void TheoryQuant::setupTriggers(ExprMap<ExprMap<vector<dynTrig>* >*>& trig_maps,
const Theorem& thm,
size_t univs_id){
const Expr& e = thm.getExpr();
TRACE("triggers","setup : ",e.toString()," || ");
// cout<<"set up "<<e<<endl;
d_univs.push_back(thm);
const std::vector<Expr>& bVarsThm = e.getVars();
if (d_hasTriggers.count(e) > 0) {
std::vector<Trigger>& new_trigs = d_fullTrigs[e];
for(size_t i=0; i<new_trigs.size(); i++){
registerTrig(trig_maps, new_trigs[i], bVarsThm, univs_id);
}
if(0 == new_trigs.size()){
std::vector<Trigger>& new_mult_trigs = d_multTrigs[e];
for(size_t j=0; j<new_mult_trigs.size(); j++){
registerTrig(trig_maps, new_mult_trigs[j], bVarsThm, univs_id);
}
}
return;
}
d_hasTriggers[e]=true;
const std::vector<Expr>& subterms = getSubTrig(e);
#ifdef DEBUG
if( CVC3::debugger.trace("triggers") ){
cout<<"===========all sub terms =========="<<endl;
for (size_t i=0; i<subterms.size(); i++){
const Expr& sub = subterms[i];
cout<<"i="<< i << " : " << findExpr(sub) << " | " << sub << " and type is " << sub.getType()
<< " and kind is " << sub.getEM()->getKindName(sub.getKind()) << endl;
}
}
#endif
ExprMap<Polarity> exprPol;
findPolarity(e, exprPol, Pos);
{
std::vector<Expr> trig_cadt;
for(std::vector<Expr>::const_iterator i = subterms.begin(),iend=subterms.end(); i!=iend; i++){
if(isGoodFullTrigger(*i, bVarsThm)) {
trig_cadt.push_back(*i);
}
}
std::vector<Expr> trig_list;
std::vector<Expr> trig_extra;
for(size_t iter =0; iter < trig_cadt.size(); iter++) {
Expr* i = &(trig_cadt[iter]);
bool notfound = true;
for(size_t index=0; index< trig_list.size(); index++){
if (i->subExprOf(trig_list[index])) {
trig_list[index]=*i;
notfound=false;
break;
}
if (trig_list[index].subExprOf(*i)) {
notfound=false;
break;
}
}
if (notfound) {
trig_list.push_back(*i);
}
}
std::vector<Trigger> trig_ex;
for (size_t i=0; i< trig_list.size();i++){
const Expr& cur = trig_list[i];
const std::set<Expr> cur_bvs = getBoundVars(cur);
int score = trigInitScore(cur);
if(score > 0) continue;
//1. test trans2
//2. test whether a trigger can trig a bigger instance of itself, now we have no actions for such case because we use expr score and dynamic loop prevention.
for(size_t j=0; j< trig_cadt.size(); j++){
if (trig_list[i] == trig_cadt[j]) continue;
ExprMap<Expr> null;
if (canMatch(trig_list[i], trig_cadt[j], null)){
if(exprScore(trig_list[i]) < exprScore(trig_cadt[j])){
}
else if(*d_useTrans2 &&
trig_list.size() == 2 &&
trig_list[i].arity() == 2 &&
BOUND_VAR == trig_list[i][0].getKind() &&
BOUND_VAR == trig_list[i][1].getKind() &&
BOUND_VAR == trig_cadt[j][0].getKind() &&
BOUND_VAR == trig_cadt[j][1].getKind() &&
isTrans2Like(subterms, trig_list[i])
){
score =0; //useless, to delete;
d_trans2_num++;
DebugAssert(d_trans2_num<=1, "more than 2 trans2 found");
TRACE("triggers", "trans2 found ", trig_list[i], "");
Trigger t(theoryCore(), cur, Neg, cur_bvs);
t.setTrans2(true);
t.setHead(getHeadExpr(cur));
if(isSimpleTrig(cur)){
t.setSimp();
}
if(isSuperSimpleTrig(cur)){
t.setSuperSimp();
}
d_fullTrigs[e].push_back(t);
registerTrig(trig_maps,t, bVarsThm, univs_id);
return;
}
else{
score =0;
}
}
}
Polarity pol= Ukn;
if(cur.getType().isBool()){
DebugAssert(exprPol.count(e)>0,"unknown polarity:"+cur.toString());
pol = exprPol[cur];
}
Trigger* t;
Trigger* t_ex; //so, if a pred is PosNeg, we actually put two triggers into the list, one pos and the other neg
if(PosNeg == pol && *d_usePolarity){
t = new Trigger(theoryCore(), cur, Pos, cur_bvs);
t_ex = new Trigger(theoryCore(), cur, Neg, cur_bvs);
if(isSimpleTrig(cur)){
t->setSimp();
t_ex->setSimp();
}
if(isSuperSimpleTrig(cur)){
t->setSuperSimp();
t_ex->setSuperSimp();
}
}
else{
t = new Trigger(theoryCore(), cur, pol, cur_bvs);
if(isSimpleTrig(cur)){
t->setSimp();
}
if(isSuperSimpleTrig(cur)){
t->setSuperSimp();
}
t_ex = NULL;
}
if(canGetHead(cur)) {
t->setHead(getHeadExpr(cur));
if(NULL != t_ex){
t_ex->setHead(getHeadExpr(cur));
}
}
else{
if(!isSysPred(cur)){
// cout<<"cur " << cur <<endl;
DebugAssert(false, "why this is a trigger");
}
}
t->setRWOp(false);
if(READ == cur.getKind() || WRITE == cur.getKind()){
arrayIndexName(cur);
}
if(READ == cur.getKind() && WRITE== cur[0].getKind() && 1 == bVarsThm.size() ){
// cout<<t->trig<<endl;
t->setRWOp(true);
if(t_ex != NULL) t_ex->setRWOp(true);
}
if(t_ex != NULL) {
trig_ex.push_back(*t_ex);
}
d_fullTrigs[e].push_back(*t);
registerTrig(trig_maps,*t, bVarsThm, univs_id);
TRACE("triggers", "new:full triggers:", cur.toString(),"");
TRACE("triggers", "new:full trigger score:", score,"");
TRACE("triggers", "new:full trigger pol:", pol,"");
}
for(size_t i=0; i<trig_ex.size(); i++){
d_fullTrigs[e].push_back(trig_ex[i]);
registerTrig(trig_maps,trig_ex[i], bVarsThm, univs_id);
TRACE("triggers", "new extra :full triggers:", trig_ex[i].getEx().toString(),"");
}
if(d_fullTrigs[e].size() == 0){
TRACE("triggers warning", "no full trig: ", e , "");
}
}
if(0 == d_fullTrigs[e].size() )
{ //setup multriggers
for( std::vector<Expr>::const_iterator i = subterms.begin(), iend=subterms.end(); i!=iend; i++) {
if(isGoodMultiTrigger(*i, bVarsThm, d_offset_multi_trig)) {
bool notfound = true;
for(size_t index=0; index<d_multTriggers[e].size(); index++){
if (i->subExprOf(d_multTriggers[e][index])) {
(d_multTriggers[e][index])=*i;
notfound=false;
}
}
if (notfound){
d_multTriggers[e].push_back(*i);
}
}
}
std::vector<Expr>& cur_trig = d_multTriggers[e];
if (goodMultiTriggers(cur_trig, bVarsThm)){
// cout<<"good multi triggers"<<endl;
TRACE("multi-triggers", "good set of multi triggers","","");
for (size_t i=0; i< d_multTriggers[e].size();i++){
// cout<<"multi-triggers" <<d_multTriggers[e][i]<<endl;
TRACE("multi-triggers", "multi-triggers:", d_multTriggers[e][i].toString(),"");
}
}
else{
cur_trig.clear();
// cout<<"bad multi triggers"<<endl;
TRACE("multi-triggers", "bad set of multi triggers","","");
}
//special code for transitive pred,
{
if(isTransLike(cur_trig)){
d_trans_num++;
DebugAssert(d_trans_num <= 1, "more than one trans found");
Expr ex = cur_trig[0];
Trigger* trans_trig = new Trigger(theoryCore(), ex, Neg, getBoundVars(ex));
trans_trig->setHead(getHeadExpr(ex));
if(isSimpleTrig(ex)){
trans_trig->setSimp();
}
if(isSuperSimpleTrig(ex)){
trans_trig->setSuperSimp();
}
trans_trig->setTrans(true);
d_fullTrigs[e].push_back(*trans_trig);
registerTrig(trig_maps,*trans_trig, bVarsThm, univs_id);
cur_trig.clear();
}
}
//enhanced multi-triggers
if(cur_trig.size() >0 ){
// if(cur_trig.size() >0 ){
std::vector<Expr> posList, negList;
for(size_t k=0; k<cur_trig.size(); k++){
const Expr& cur_item = cur_trig[k];
if (cur_item.getType().isBool()){
Polarity pol = exprPol[cur_item];
if(PosNeg == pol || Pos == pol){
posList.push_back(cur_item);
}
if(PosNeg == pol || Neg == pol){
negList.push_back(cur_item);
}
}
}
if (goodMultiTriggers(posList, bVarsThm)){
TRACE("multi-triggers", "good set of multi triggers pos","","");
for (size_t i=0; i< posList.size();i++){
TRACE("multi-triggers", "multi-triggers:", posList[i].toString(),"");
}
cur_trig.clear();
for(size_t m=0; m<posList.size(); m++){
cur_trig.push_back(posList[m]);
}
}
if (goodMultiTriggers(negList, bVarsThm) && negList.size() < cur_trig.size()){
TRACE("multi-triggers", "good set of multi triggers neg","","");
for (size_t i=0; i< negList.size();i++){
TRACE("multi-triggers", "multi-triggers:", negList[i].toString(),"");
}
cur_trig.clear();
for(size_t m=0; m<negList.size(); m++){
cur_trig.push_back(negList[m]);
}
}
// cout<<"neg list and pos list"<<negList.size()<<" | " <<posList.size()<<endl;
}
{//new way of multi trigger
if( 3 == cur_trig.size() || 4 == cur_trig.size() || 5 == cur_trig.size() || 6 == cur_trig.size() ){
for(size_t i = 0; i < cur_trig.size(); i++){
for(size_t j = 0; j < i; j++){
vector<Expr> tempList;
tempList.clear();
tempList.push_back(cur_trig[i]);
tempList.push_back(cur_trig[j]);
// cout<<i<<" | "<<j<<endl;
// cout<<vectorExpr2string(tempList)<<endl;
if (goodMultiTriggers(tempList, bVarsThm)){
cur_trig.clear();
cur_trig.push_back(tempList[0]);
cur_trig.push_back(tempList[1]);
break;
}
}
}
}
if(cur_trig.size() != 2){
if( 0 == cur_trig.size()){
return;
}
// FatalAssert(false, "unsupported multi-triggers");
// cout<<"e: "<<e<<endl;
// cout<<cur_trig.size()<<endl;
// cout<<bVarsThm.size()<<endl;
//
// cout<<vectorExpr2string(bVarsThm)<<endl;
// for(size_t i =0; i<cur_trig.size(); i++){
// cout<<cur_trig[i]<<endl;
// }
return;
}
for(size_t i = 0 ; i<cur_trig.size(); i++){
set<Expr> bvs = getBoundVars(cur_trig[i]);
Trigger trig(theoryCore(), cur_trig[i], Ukn, bvs); //
trig.setHead(getHead(cur_trig[i]));
trig.setMultiTrig();
trig.multiIndex = i;
trig.multiId=d_all_multTrigsInfo.size();
d_multTrigs[e].push_back(trig);
registerTrig(trig_maps, trig, bVarsThm, univs_id);
}
{
multTrigsInfo multTrigs;
for(size_t i =0, iend = d_multTrigs[e].size(); i<iend; i++){
const std::vector<Expr>& one_set_bvs = d_multTrigs[e][i].bvs;
std::vector<size_t> one_set_pos;
for(size_t v = 0, vend = one_set_bvs.size(); v<vend; v++){
size_t loc = locVar(bVarsThm, one_set_bvs[v]);
if( 999 != loc ){
one_set_pos.push_back(loc);
}
}
sort(one_set_pos.begin(), one_set_pos.end());
for(size_t v = 0, vend = one_set_pos.size(); v<vend; v++){
}
multTrigs.var_pos.push_back(one_set_pos);
}//setup pos of all multi tirggers
//now we only consider two multi triggers
vector<size_t> common;
std::vector<size_t>& tar1 = multTrigs.var_pos[0];
std::vector<size_t>& tar2 = multTrigs.var_pos[1];
vector<size_t>::iterator t1(tar1.begin()), t2(tar2.begin());
while(t1 != tar1.end() && t2!= tar2.end()){
size_t pos1 = *t1;
size_t pos2 = *t2;
if( pos1 == pos2 ) {
common.push_back(pos1);
t1=tar1.erase(t1);
t2=tar2.erase(t2);
}
else if( pos1 > pos2 ){
t2++;
}
else {
t1++;
}
}
multTrigs.common_pos.push_back(common);
size_t multi_size = d_multTrigs[e].size(); //should be 2
for(size_t i =0; i< multi_size; i++){
multTrigs.var_binds_found.push_back(new (true) CDMap<Expr, bool> (theoryCore()->getCM()->getCurrentContext()));
}
multTrigs.uncomm_list.push_back(new ExprMap<CDList<Expr>* >);
multTrigs.uncomm_list.push_back(new ExprMap<CDList<Expr>* >);
d_multitrigs_maps[e]=multTrigs;
d_all_multTrigsInfo.push_back(multTrigs);
}
}
}
//setup partial triggers
if(*d_usePart)
{
std::vector<Trigger> trig_ex;
trig_ex.clear();
for( std::vector<Expr>::const_iterator i = subterms.begin(), iend=subterms.end(); i!=iend; i++) {
if(isGoodPartTrigger(*i, bVarsThm)) {
bool notfound = true;
for(size_t index=0; index<d_partTriggers[e].size(); index++){
if (i->subExprOf(d_partTriggers[e][index])) {
(d_partTriggers[e][index])=*i;
notfound=false;
}
}
if (notfound)
d_partTriggers[e].push_back(*i);
}
}
for (size_t i=0; i< d_partTriggers[e].size();i++){
TRACE("triggers", "partial triggers:", d_partTriggers[e][i].toString(),"");
}
for (size_t i=0; i< d_partTriggers[e].size();i++){
Polarity pol= Ukn;
const Expr& cur = d_partTriggers[e][i];
const std::set<Expr> cur_bvs = getBoundVars(cur);
if(cur.getType().isBool()){
DebugAssert(exprPol.count(e)>0,"unknown polarity:"+cur.toString());
pol = exprPol[cur];
}
Trigger* t;
Trigger* t_ex; //so, if a pred is PosNeg, we actually put two triggers into the list, one pos and the other neg
if(PosNeg == pol && *d_usePolarity){
t = new Trigger(theoryCore(), cur, Pos, cur_bvs);
t_ex = new Trigger(theoryCore(), cur, Neg, cur_bvs);
}
else{
t = new Trigger(theoryCore(), cur, pol, cur_bvs);
t_ex = NULL;
}
if(canGetHead(cur)) {
t->setHead(getHeadExpr(cur));
}
if(t_ex != NULL) trig_ex.push_back(*t_ex);
d_partTrigs[e].push_back(*t);
TRACE("triggers", "new:part trigger pol:", pol,cur.toString());
}
for(size_t i=0; i<trig_ex.size(); i++){
d_partTrigs[e].push_back(trig_ex[i]);
TRACE("triggers", "new extra :part triggers:", trig_ex[i].getEx().toString(),"");
}
}
}
//! test if a sub-term contains more bounded vars than quantified by out-most quantifier.
int hasMoreBVs(const Expr& thm){
DebugAssert(thm.isForall(), "hasMoreBVS called by non-forall exprs");
const std::vector<Expr>& bvsOutmost = thm.getVars();
const std::set<Expr>& bvs = getBoundVars(thm);
return int(bvs.size()-bvsOutmost.size());
}
/*! \brief Theory interface function to assert quantified formulas
*
* pushes in negations and converts to either universally or existentially
* quantified theorems. Universals are stored in a database while
* existentials are enqueued to be handled by the search engine.
*/
void TheoryQuant::assertFact(const Theorem& thm){
if(*d_translate) return;
TRACE("quant assertfact", "assertFact => ", thm.toString(), "{");
Theorem rule, result;
const Expr& expr = thm.getExpr();
// Ignore existentials
if(expr.isExists()) {
TRACE("quant assertfact", "assertFact => (ignoring existential) }", expr.toString(), "");
return;
}
DebugAssert(expr.isForall() || (expr.isNot() && (expr[0].isExists() || expr[0].isForall())),
"Theory of quantifiers cannot handle expression "
+ expr.toString());
if(expr.isNot()) {//find the right rule to eliminate negation
if(expr[0].isForall()) {
rule = d_rules->rewriteNotForall(expr);
}
else if(expr[0].isExists()) {
rule = d_rules->rewriteNotExists(expr);
}
result = iffMP(thm, rule);
}
else{
result = thm;
}
result = d_rules->boundVarElim(result); //eliminate useless bound variables
if(result.getExpr().isForall()){
if(*d_useNew){
if(result.getExpr().getBody().isForall()){ // if it is of the form forall x. forall. y
result=d_rules->packVar(result);
}
result = d_rules->boundVarElim(result); //eliminate useless bound variables
int nBVs = hasMoreBVs(result.getExpr());
if( nBVs >= 1){
d_hasMoreBVs[result.getExpr()]=true;
}
d_rawUnivs.push_back(result);
return;
/* -------------------------------------- */
// int nBVs = hasMoreBVs(result.getExpr());
if(0 == nBVs){//good
TRACE("quant assertfact", "assertFact => forall enqueueing: ", result.toString(), "}");
d_univs.push_back(result);
setupTriggers(result, d_univs.size()-1);
}
else if(1== nBVs){
d_hasMoreBVs[result.getExpr()]=true;
const Expr& body = result.getExpr().getBody();
if(*d_usePullVar){
if((body.isAnd() && body[1].isForall()) || (body.isImpl() && body[1].isForall()) ){
result=d_rules->pullVarOut(result);
TRACE("quant assertfact", "assertFact => pull-var enqueueing: ", result.toString(), "}");
d_univs.push_back(result);
setupTriggers(result, d_univs.size()-1);
}
}
else{
TRACE("quant assertfact", "debug:not recognized case", result.toString(), thm.toString());
d_univs.push_back(result);
setupTriggers(result, d_univs.size()-1);
return;
}
}
else{
d_hasMoreBVs[result.getExpr()]=true;
d_univs.push_back(result);
setupTriggers(result, d_univs.size()-1);
return;
}
}
else{
TRACE("quant assertfact", "assertFact => old-fashoin enqueueing: ", result.toString(), "}");
// cout<<"error"<<endl;
d_univs.push_back(result);
}
}
else { //quantifier got eliminated or is an existantial formula
TRACE("quant assertfact", "assertFact => non-forall enqueueing: ", result.toString(), "}");
enqueueFact(result);
}
}
void TheoryQuant::recGoodSemMatch(const Expr& e,
const std::vector<Expr>& bVars,
std::vector<Expr>& newInst,
std::set<std::vector<Expr> >& instSet)
{
size_t curPos = newInst.size();
if (bVars.size() == curPos) {
Expr simpleExpr = simplifyExpr(e.substExpr(bVars,newInst));
if (simpleExpr.hasFind()){
std::vector<Expr> temp = newInst;
instSet.insert(temp);
TRACE("quant yeting", "new inst found for ", e.toString()+" ==> ", simpleExpr.toString());
};
}
else {
Type t = getBaseType(bVars[curPos]);
std::vector<Expr> tyExprs= d_typeExprMap[t];
if (0 == tyExprs.size()) {
return;//has some problem
}
else{
for (size_t i=0;i<tyExprs.size();i++){
newInst.push_back(tyExprs[i]);
recGoodSemMatch(e,bVars,newInst,instSet);
newInst.pop_back();
}
}
}
}
bool isIntx(const Expr& e, const Rational& x){
if(e.isRational() && e.getRational()==x)
return true;
else return false;
}
Expr getLeft(const Expr& e){
if(e.getKind()!= PLUS) return null_expr;
if(e.arity() != 3) return null_expr;
Expr const_expr, minus ,pos;
int numMinus=0, numPos=0, numConst=0;;
for(int i=0; i<e.arity(); i++){
if((e[i]).getKind() == MULT){
if(isIntx(e[i][0], -1)){
numMinus++;
minus=e[i][1];
}
else{
numPos++;
pos=e[i];
}
}
else if(e[i].isRational()) {
const_expr = e[i];
numConst++;
}
else{
numPos++;
pos=e[i];
}
}
if(1==numPos && 1==numConst && 1==numMinus){
return minus;
}
else{
return null_expr;
}
}
Expr getRight(const Expr& e){
if(e.getKind()!= PLUS) return null_expr;
if(e.arity() != 3) return null_expr;
Expr const_expr, minus ,pos;
int numMinus=0, numPos=0, numConst=0;;
for(int i=0; i<e.arity(); i++){
if((e[i]).getKind() == MULT){
if(isIntx(e[i][0], -1)){
numMinus++;
minus=e[i][1];
}
else{
numPos++;
pos=e[i];
}
}
else if(e[i].isRational()) {
const_expr = e[i];
numConst++;
}
else{
numPos++;
pos=e[i];
}
}
if(1==numPos && 1==numConst && 1==numMinus){
if(isIntx(const_expr,0)){
return pos;
}
else{
// return null_expr;
return Expr(PLUS, const_expr, pos);
}
}
else{
return null_expr;
}
}
inline void TheoryQuant::add_parent(const Expr& parent){
ExprMap<CDList<Expr>* >::iterator iter;
for(int i=0; i< parent.arity(); i++){
const Expr& child = parent[i];
iter = d_parent_list.find(child);
if(d_parent_list.end() == iter){
d_parent_list[child] = new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
d_parent_list[child]->push_back(parent);
}
else{
iter->second->push_back(parent);
}
}
}
void TheoryQuant::collectChangedTerms(CDList<Expr>& changed){
ExprMap<bool> eqs_hash;
ExprMap<bool> changed_hash;
/*
{
for(ExprMap<CDList<Expr>* >::iterator iter = d_eq_list.begin(), iter_end=d_eq_list.end();
iter != iter_end; iter++){
CDList<Expr>* cur_eqs = iter->second;
int begin_pos;
Expr head = iter->first;
if(d_eq_pos.find(head) == d_eq_pos.end()){
begin_pos=0;
d_eq_pos[head]= new(true) CDO<size_t>(theoryCore()->getCM()->getCurrentContext(), 0, 0);
}
else{
begin_pos = *(d_eq_pos[head]);
}
for(size_t i=begin_pos; i<cur_eqs->size(); i++){
eqs_hash[(*cur_eqs)[i]]=true;
}
(d_eq_pos[head])->set(cur_eqs->size());
}
}*/
for(size_t i=d_eqs_pos; i<d_eqs.size(); i++){
eqs_hash[d_eqs[i]]=true;
}
d_eqs_pos.set(d_eqs.size());
{
for(ExprMap<bool>::iterator iter = eqs_hash.begin(), iter_end = eqs_hash.end(); iter != iter_end; iter++){
const Expr& cur_ex = iter->first;
ExprMap<CDList<Expr>* >::iterator iter_parent = d_parent_list.find(cur_ex);
if(d_parent_list.end() != iter_parent){
CDList<Expr>* cur_parents = iter_parent->second;
for(size_t i=0; i<cur_parents->size(); i++){
changed_hash[(*cur_parents)[i]]=true;
}
}
}
}
{
for(ExprMap<bool>::iterator iter = changed_hash.begin(), iter_end = changed_hash.end(); iter != iter_end; iter++){
changed.push_back(iter->first);
}
}
}
inline bool TheoryQuant::matchChild(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env){
if(gterm.arity() != vterm.arity()) {
return false;
}
for(int i = 0 ; i< gterm.arity(); i++){
const Expr& cur_v = vterm[i];
const Expr& cur_g = gterm[i];
if(BOUND_VAR == cur_v.getKind()){
ExprMap<Expr>::iterator p = env.find(cur_v);
if ( p != env.end()){
if (simplifyExpr(cur_g) != simplifyExpr(p->second)){
return false;
}
}
else {
env[cur_v] = simplifyExpr(cur_g);
}
}
else if (!cur_v.containsBoundVar()){
if(simplifyExpr(cur_v) != simplifyExpr(cur_g)){
return false;
}
}
else{
if (false == recSynMatch(cur_g, cur_v, env)){
return false;
}
}
}
return true;
}
inline void TheoryQuant::matchChild(const Expr& gterm, const Expr& vterm, vector<ExprMap<Expr> >& binds){
ExprMap<Expr> env;
if(gterm.arity() != vterm.arity()) {
return;
}
for(int i = 0 ; i< gterm.arity(); i++){
const Expr& cur_v = vterm[i];
const Expr& cur_g = gterm[i];
if(BOUND_VAR == cur_v.getKind()){
ExprMap<Expr>::iterator p = env.find(cur_v);
if ( p != env.end()){
if (simplifyExpr(cur_g) != simplifyExpr(p->second)){
return;
}
}
else {
env[cur_v] = simplifyExpr(cur_g);
}
}
else if (!cur_v.containsBoundVar()){
if(simplifyExpr(cur_v) != simplifyExpr(cur_g)){
return ;
}
}
else{
if (false == recSynMatch(cur_g, cur_v, env)){
return;
}
}
}
binds.push_back(env);
return;
}
//match a gterm against all the trigs in d_allmap_trigs
void TheoryQuant::matchListOld(const CDList<Expr>& glist, size_t gbegin, size_t gend){
for(size_t g_index = gbegin; g_index < gend; g_index++){
const Expr& gterm = glist[g_index];
if(gterm.isEq()){
continue; // we do not match with equality
}
Expr head = getHead(gterm);
ExprMap<CDMap<Expr, CDList<dynTrig>* > *>::iterator iter = d_allmap_trigs.find(head);
if(d_allmap_trigs.end() == iter) continue;
CDMap<Expr, CDList<dynTrig>*>* cd_map = iter->second;
// if(cd_map->size()>10){
// cout<<"map size1:"<<cd_map->size()<<endl;
// cout<<head<<endl;
// }
CDMap<Expr, CDList<dynTrig>*>::iterator iter_trig = (*cd_map).begin();
CDMap<Expr, CDList<dynTrig>*>::iterator iter_trig_end = (*cd_map).end();
for(;iter_trig != iter_trig_end; iter_trig++){
CDList<dynTrig>* cur_list = (*iter_trig).second;
if(1 == cur_list->size() || null_expr == head || gterm.getType().isBool()){
for(size_t cur_index =0; cur_index < cur_list->size(); cur_index++){
const Trigger& cur_trig = (*cur_list)[cur_index].trig;
size_t univ_id = (*cur_list)[cur_index].univ_id;
vector<ExprMap<Expr> > binds;
const Expr& vterm = cur_trig.trig;
if ( d_allout && cur_trig.isSuperSimple && !cur_trig.hasTrans && !cur_trig.isMulti) continue;
// if ( d_allout && cur_trig.isSimple ) continue;
newTopMatch(gterm, vterm, binds, cur_trig);
for(size_t i=0; i<binds.size(); i++){
ExprMap<Expr>& cur_map = binds[i];
vector<Expr> bind_vec;
const vector<Expr>& bVarsThm = d_univs[univ_id].getExpr().getVars();
for(size_t j=0; j< bVarsThm.size(); j++){
bind_vec.push_back(cur_map[bVarsThm[j]]);
}
synNewInst(univ_id, bind_vec, gterm, cur_trig);
}
}
}
else if ( cur_list->size() > 1){
const Trigger& cur_trig = (*cur_list)[0].trig;//here we have a polarity problem
const Expr& general_vterm = (*iter_trig).first;
vector<ExprMap<Expr> > binds;
if ( d_allout && cur_trig.isSuperSimple && !cur_trig.hasTrans && !cur_trig.isMulti) continue;
//if ( d_allout && cur_trig.isSimple ) continue;
newTopMatch(gterm, general_vterm, binds, cur_trig);
for(size_t trig_index = 0; trig_index< cur_list->size(); trig_index++){
size_t univ_id = (*cur_list)[trig_index].univ_id;
const ExprMap<Expr>& trig_map = (*cur_list)[trig_index].binds;
const Trigger& ind_cur_trig = (*cur_list)[trig_index].trig;
for(size_t i=0; i<binds.size(); i++){
ExprMap<Expr>& cur_map = binds[i];
vector<Expr> bind_vec;
const vector<Expr>& bVarsThm = d_univs[univ_id].getExpr().getVars();
for(size_t j=0; j< bVarsThm.size(); j++){
const Expr& inter=(*(trig_map.find(bVarsThm[j]))).second;
const Expr& inter2 = cur_map[inter];
bind_vec.push_back(inter2);
}
synNewInst(univ_id, bind_vec, gterm, ind_cur_trig);
}
}
}
else{
FatalAssert(false, "error in matchlistold");
}
}//end of for each trig begins with head
}//end of each gterm
}
void TheoryQuant::delNewTrigs(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs){
//return;
ExprMap<ExprMap<std::vector<dynTrig>*>*>::iterator i = new_trigs.begin();
ExprMap<ExprMap<std::vector<dynTrig>*>*>::iterator iend = new_trigs.end();
for(; i!=iend; i++){
ExprMap<std::vector<dynTrig>*>* cur_new_cd_map = i->second;
ExprMap<vector<dynTrig>* >::iterator j = cur_new_cd_map->begin();
ExprMap<vector<dynTrig>* >::iterator jend = cur_new_cd_map->end();
for(; j!=jend; j++){
Expr general_trig = j->first;
vector<dynTrig>* trigs = j->second;
delete trigs;
}
delete cur_new_cd_map;
}
new_trigs.clear();
}
void TheoryQuant::combineOldNewTrigs(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs){
ExprMap<ExprMap<std::vector<dynTrig>*>*>::iterator i = new_trigs.begin();
ExprMap<ExprMap<std::vector<dynTrig>*>*>::iterator iend = new_trigs.end();
for(; i!=iend; i++){
ExprMap<std::vector<dynTrig>*>* cur_new_cd_map = i->second;
Expr head = i->first;
ExprMap<CDMap<Expr, CDList<dynTrig>* >* >::iterator old_iter = d_allmap_trigs.find(head);
if(d_allmap_trigs.end() == old_iter){
CDMap<Expr, CDList<dynTrig>* >* old_cd_map =
// new(true) CDMap<Expr, CDList<dynTrig>* > (theoryCore()->getCM()->getCurrentContext());
new(false) CDMap<Expr, CDList<dynTrig>* > (theoryCore()->getCM()->getCurrentContext());
d_allmap_trigs[head] = old_cd_map;
ExprMap<vector<dynTrig>* >::iterator j = cur_new_cd_map->begin();
ExprMap<vector<dynTrig>* >::iterator jend = cur_new_cd_map->end();
for(; j!=jend; j++){
Expr general_trig = j->first;
vector<dynTrig>* trigs = j->second;
CDList<dynTrig>* old_cd_list =
//new(true) CDList<dynTrig> (theoryCore()->getCM()->getCurrentContext());
new(false) CDList<dynTrig> (theoryCore()->getCM()->getCurrentContext());
(*old_cd_map)[general_trig] = old_cd_list;
for(size_t k=0; k<trigs->size(); k++){
(*old_cd_list).push_back((*trigs)[k]);
// cout<<"combined 1 "<<(*trigs)[k].trig.getEx()<<endl;
}
// delete trigs;
}
// delete cur_new_cd_map;
}
else{
CDMap<Expr, CDList<dynTrig>* >* old_cd_map = old_iter->second;
ExprMap<std::vector<dynTrig>*>::iterator j = cur_new_cd_map->begin();
ExprMap<std::vector<dynTrig>*>::iterator jend = cur_new_cd_map->end();
for(; j!=jend; j++){
Expr general_trig = j->first;
vector<dynTrig>* trigs = j->second;
CDMap<Expr, CDList<dynTrig>* >::iterator old_trigs_iter = old_cd_map->find(general_trig);
CDList<dynTrig>* old_cd_list;
if(old_cd_map->end() == old_trigs_iter){
old_cd_list =
//new(true) CDList<dynTrig> (theoryCore()->getCM()->getCurrentContext());
new(false) CDList<dynTrig> (theoryCore()->getCM()->getCurrentContext());
(*old_cd_map)[general_trig] = old_cd_list;
}
else{
old_cd_list = (*old_trigs_iter).second;
}
for(size_t k=0; k<trigs->size(); k++){
(*old_cd_list).push_back((*trigs)[k]);
// cout<<"combined 2 "<<(*trigs)[k].trig.getEx()<<endl;
}
// delete trigs;
}
// delete cur_new_cd_map;
}
}
delNewTrigs(new_trigs);
// new_trigs.clear();
}
//match a gterm against all the trigs in d_allmap_trigs
void TheoryQuant::matchListNew(ExprMap<ExprMap<vector<dynTrig>*>*>& new_trigs,
const CDList<Expr>& glist,
size_t gbegin,
size_t gend){
for(size_t g_index = gbegin; g_index<gend; g_index++){
const Expr& gterm = glist[g_index];
if(gterm.isEq()){
continue; // we do not match with equality
}
Expr head = getHead(gterm);
ExprMap<ExprMap<vector<dynTrig>* > *>::iterator iter = new_trigs.find(head);
if(new_trigs.end() == iter) continue;
ExprMap<vector<dynTrig>*>* cd_map = iter->second;
// if(cd_map->size()>10){
// cout<<"map size2:"<<cd_map->size()<<endl;
// cout<<head<<endl;
// }
ExprMap<vector<dynTrig>*>::iterator iter_trig = (*cd_map).begin();
ExprMap<vector<dynTrig>*>::iterator iter_trig_end = (*cd_map).end();
for(;iter_trig != iter_trig_end; iter_trig++){
vector<dynTrig>* cur_list = (*iter_trig).second;
if(1 == cur_list->size() || null_expr == head || gterm.getType().isBool()){
for(size_t cur_index =0; cur_index < cur_list->size(); cur_index++){
const Trigger& cur_trig = (*cur_list)[cur_index].trig;
// if ( d_allout && cur_trig.isSuperSimple && !cur_trig.hasTrans) continue;
size_t univ_id = (*cur_list)[cur_index].univ_id;
vector<ExprMap<Expr> > binds;
const Expr& vterm = cur_trig.trig;
newTopMatch(gterm, vterm, binds, cur_trig);
for(size_t i=0; i<binds.size(); i++){
ExprMap<Expr>& cur_map = binds[i];
vector<Expr> bind_vec;
const vector<Expr>& bVarsThm = d_univs[univ_id].getExpr().getVars();
for(size_t j=0; j< bVarsThm.size(); j++){
bind_vec.push_back(cur_map[bVarsThm[j]]);
}
synNewInst(univ_id, bind_vec, gterm, cur_trig);
}
}
}
else if ( cur_list->size() > 1){
const Trigger& cur_trig = (*cur_list)[0].trig;//here we have a polarity problem
// if ( d_allout && cur_trig.isSuperSimple && !cur_trig.hasTrans) continue;
const Expr& general_vterm = (*iter_trig).first;
vector<ExprMap<Expr> > binds;
newTopMatch(gterm, general_vterm, binds, cur_trig);
for(size_t trig_index = 0; trig_index< cur_list->size(); trig_index++){
size_t univ_id = (*cur_list)[trig_index].univ_id;
const Trigger& ind_cur_trig = (*cur_list)[trig_index].trig;
const ExprMap<Expr>& trig_map = (*cur_list)[trig_index].binds;
for(size_t i=0; i<binds.size(); i++){
ExprMap<Expr>& cur_map = binds[i];
vector<Expr> bind_vec;
const vector<Expr>& bVarsThm = d_univs[univ_id].getExpr().getVars();
for(size_t j=0; j< bVarsThm.size(); j++){
const Expr& inter=(*(trig_map.find(bVarsThm[j]))).second;
const Expr& inter2 = cur_map[inter];
bind_vec.push_back(inter2);
}
synNewInst(univ_id, bind_vec, gterm, ind_cur_trig);
}
}
}
else{
FatalAssert(false, "error in matchlistold");
}
}//end of for each trig begins with head
}// end of each gterm
}
void TheoryQuant::newTopMatch(const Expr& gterm,
const Expr& vterm,
vector<ExprMap<Expr> >& binds,
const Trigger& trig){
ExprMap<Expr> cur_bind;
if(trig.isSuperSimple){
for(int i = vterm.arity()-1; i>=0 ; i--){
cur_bind[vterm[i]] = simplifyExpr(gterm[i]);
}
binds.push_back(cur_bind);
return;
}
if(trig.isSimple){
for(int i = vterm.arity()-1; i>=0 ; i--){
if(BOUND_VAR != vterm[i].getKind()){
if(simplifyExpr(gterm[i]) != simplifyExpr(vterm[i])) {
return ;
}
}
else{
cur_bind[vterm[i]] = simplifyExpr(gterm[i]);
}
}
binds.push_back(cur_bind);
return;
}
if(!isSysPred(vterm)){ //then gterm cannot be a syspred
if(!gterm.getType().isBool()){
// res2= recSynMatch(gterm, vterm, env);
matchChild(gterm, vterm, binds);
return;
}
matchChild(gterm, vterm, binds);
return;
if(!*d_usePolarity){
// return recSynMatch(gterm, vterm, env);
matchChild(gterm, vterm, binds);
return;
}
const bool gtrue = (trueExpr()==findExpr(gterm));
// const bool gtrue = (trueExpr()==simplifyExpr(gterm));
if(gtrue ){
if((Neg==trig.polarity || PosNeg==trig.polarity)) {
// return recSynMatch(gterm, vterm, env);
matchChild(gterm, vterm, binds);
return;
}
else{
// cout<<"returned 1"<<endl;
return;
}
}
const bool gfalse = (falseExpr()==findExpr(gterm));
//const bool gfalse = (falseExpr()==simplifyExpr(gterm));
if(gfalse){
if((Pos==trig.polarity || PosNeg==trig.polarity)) {
// return recSynMatch(gterm, vterm, env);
matchChild(gterm, vterm, binds); //it is possible that we need binds here, not a single bind
return;
}
else{
// cout<<"returned 2"<<endl;
return;
}
}
// cout<<"immpossible here in new top match"<<endl;
// cout<<"vterm "<<vterm<<endl;
// cout<<trig.polarity<<endl;
// cout<<gtrue<<" | " <<gfalse<<endl;
// cout<<"gterm " <<gterm<<endl;
// cout<<"gterm " <<simplifyExpr(gterm)<<endl;
matchChild(gterm, vterm, binds);
return;
return;
}
else{ // must be syspreds
//we can move the work to split vterm into left and right into setuptriggers
Expr gl = getLeft(gterm[1]);
Expr gr = getRight(gterm[1]);
if(null_expr == gr || null_expr == gl){
gl = gterm[0];
gr = gterm[1];
}
Expr vr, vl;
Expr tvr, tvl;
tvr=null_expr;
tvl=null_expr;
if(isGE(vterm) || isGT(vterm)){
vr = vterm[0];
vl = vterm[1];
}
else if(isLE(vterm) || isLT(vterm)){
vr = vterm[1];
vl = vterm[0];
}
else{
FatalAssert(false, "impossilbe in toppred");
}
if(isIntx(vl,0)){
tvl = getLeft(vr);
tvr = getRight(vr);
}
else if(isIntx(vr,0)) {
tvl = getLeft(vl);
tvr = getRight(vl);
}
if( (null_expr != tvl) && (null_expr != tvr)){
vl = tvl;
vr = tvr;
}
const bool gtrue = (trueExpr()==findExpr(gterm));
const bool gfalse = (falseExpr()==findExpr(gterm));
TRACE("quant toppred"," vl, gl, vr, gr:", vl.toString()+"::"+gl.toString()+"||", vr.toString()+"::"+gr.toString());
// DebugAssert(!(trig.isNeg() && trig.isPos()), "expr in both pos and neg");
if(!*d_usePolarity){
if((recSynMatch(gl, vl, cur_bind) && recSynMatch(gr, vr, cur_bind))){
binds.push_back(cur_bind); // it is possible that cur_bind will be binds
return;
}
else{
return;
}
}
if((Neg==trig.polarity || PosNeg==trig.polarity)) {
if (( gtrue ) ) {
if (recSynMatch(gl, vl, cur_bind) && recSynMatch(gr, vr, cur_bind)){
binds.push_back(cur_bind);
return;
}
else{
return;
}
}
else {
if(recSynMatch(gl, vr, cur_bind) && recSynMatch(gr, vl, cur_bind)){
binds.push_back(cur_bind);
return;
}
else{
return;
}
}
}
else if((Pos==trig.polarity || PosNeg==trig.polarity)) {
if (( gfalse )) {
if(recSynMatch(gl, vl, cur_bind) && recSynMatch(gr, vr, cur_bind)){
binds.push_back(cur_bind);
return;
}
else{
return;
}
}
else {
if(recSynMatch(gl, vr, cur_bind) && recSynMatch(gr, vl, cur_bind)){
binds.push_back(cur_bind);
return;
}
else{
return;
}
}
}
else {
FatalAssert(false, "impossible polarity for trig");
//DebugAssert(false, "impossible polarity for trig");
// res = false;
return;
}
}
}
/*
bool TheoryQuant::synMatchTopPred(const Expr& gterm, Trigger trig, ExprMap<Expr>& env){
Expr vterm = trig.getEx();
TRACE("quant toppred", "top pred: gterm:| "+gterm.toString()," vterm:| "+vterm.toString(),"");
DebugAssert ((BOUND_VAR != gterm.getKind()),"gound term "+gterm.toString()+" has bound var");
DebugAssert ((BOUND_VAR != vterm.getKind()),"top pred match "+gterm.toString()+" has bound var");
if(gterm.isEq() || vterm.isEq()){
return false; // we do not match with equality
}
bool res2=false;
if(vterm.arity() != gterm.arity()) return false;
if(trig.isSuperSimp()){
if(trig.getHead() == getHead(gterm) ){
for(int i = vterm.arity()-1; i>=0 ; i--){
env[vterm[i]] = simplifyExpr(gterm[i]);
}
return true;
}
return false;
}
if(trig.isSimp()){
if(trig.getHead() == getHead(gterm) ){
for(int i = vterm.arity()-1; i>=0 ; i--){
if(BOUND_VAR != vterm[i].getKind()){
if(simplifyExpr(gterm[i]) != simplifyExpr(vterm[i])) {
return false;
}
}
}
for(int i = vterm.arity()-1; i>=0 ; i--){
if(BOUND_VAR == vterm[i].getKind()){
if(d_allout){
env[vterm[i]] = simplifyExpr(gterm[i]);
}
else {
env[vterm[i]] = simplifyExpr(gterm[i]);
}
}
}
return true;
}
else{
return false;
}
}
if(!(isSysPred(vterm) && isSysPred(gterm))){
if(isSysPred(vterm) || isSysPred(gterm)) {
return false;
}
if(!usefulInMatch(gterm)){
return false;
}
if(trig.getHead() != getHead(gterm)){
return false;
}
if(!gterm.getType().isBool()){
// res2= recSynMatch(gterm, vterm, env);
res2= matchChild(gterm, vterm, env);
return res2;
}
if(!*d_usePolarity){
// return recSynMatch(gterm, vterm, env);
return matchChild(gterm, vterm, env);
}
const bool gtrue = (trueExpr()==findExpr(gterm));
if(gtrue ){
if(trig.isNeg()) {
// return recSynMatch(gterm, vterm, env);
return matchChild(gterm, vterm, env);
}
else{
return false;
}
}
const bool gfalse = (falseExpr()==findExpr(gterm));
if(gfalse){
if (trig.isPos()){
// return recSynMatch(gterm, vterm, env);
return matchChild(gterm, vterm, env);
}
else{
return false;
}
}
else {
return false;
}
}
else{
DebugAssert((2==gterm.arity() && 2==vterm.arity()), "impossible situation in top pred");
DebugAssert(!((isLE(gterm) || isLT(gterm)) && !isIntx(gterm[0],0)), "canonical form changed");
#ifdef DEBUG
if( CVC3::debugger.trace("quant toppred") ){
cout << "toppred gterm, vterm" << gterm << "::" << vterm << endl;
cout << findExpr(gterm) << "::" << trig.isPos() << "|" << trig.isNeg() << endl;
}
#endif
Expr gl = getLeft(gterm[1]);
Expr gr = getRight(gterm[1]);
if(null_expr == gr || null_expr == gl){
gl = gterm[0];
gr = gterm[1];
}
Expr vr, vl;
Expr tvr, tvl;
tvr=null_expr;
tvl=null_expr;
if(isGE(vterm) || isGT(vterm)){
vr = vterm[0];
vl = vterm[1];
}
else if(isLE(vterm) || isLT(vterm)){
vr = vterm[1];
vl = vterm[0];
}
else{
DebugAssert(false, "impossilbe in toppred");
}
if(isIntx(vl,0)){
tvl = getLeft(vr);
tvr = getRight(vr);
}
else if(isIntx(vr,0)) {
tvl = getLeft(vl);
tvr = getRight(vl);
}
if( (null_expr != tvl) && (null_expr != tvr)){
vl = tvl;
vr = tvr;
}
const bool gtrue = (trueExpr()==findExpr(gterm));
const bool gfalse = (falseExpr()==findExpr(gterm));
TRACE("quant toppred"," vl, gl, vr, gr:", vl.toString()+"::"+gl.toString()+"||", vr.toString()+"::"+gr.toString());
bool res;
DebugAssert(!(trig.isNeg() && trig.isPos()), "expr in both pos and neg");
if(!*d_usePolarity){
return (recSynMatch(gl, vl, env) && recSynMatch(gr, vr, env));
}
if(trig.isNeg()){
if (( gtrue ) ) {
res=(recSynMatch(gl, vl, env) && recSynMatch(gr, vr, env));
}
else {
res=(recSynMatch(gl, vr, env) && recSynMatch(gr, vl, env));
}
}
else if(trig.isPos()){
if (( gfalse )) {
res=(recSynMatch(gl, vl, env) && recSynMatch(gr, vr, env));
}
else {
res=(recSynMatch(gl, vr, env) && recSynMatch(gr, vl, env));
}
}
else {
DebugAssert(false, "impossible polarity for trig");
res = false;
}
#ifdef DEBUG
if( CVC3::debugger.trace("quant toppred") ){
cout<<"res| "<< res << " | " << gtrue << " | " << gfalse << endl;
}
#endif
return res;
}
}
*/
bool TheoryQuant::recSynMatch(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env){
TRACE("quant match", "gterm:| "+gterm.toString()," vterm:| "+vterm.toString(),"");
DebugAssert ((BOUND_VAR != gterm.getKind()),"gound term "+gterm.toString()+" has bound var");
if (BOUND_VAR == vterm.getKind() ) {
TRACE("quant match", "bound var found;", vterm.toString(),"");
ExprMap<Expr>::iterator p = env.find(vterm);
if ( p != env.end()){
if (simplifyExpr(gterm) != simplifyExpr(p->second)){
return false;
}
else
return true;
}
else {
env[vterm] = simplifyExpr(gterm);
return true;
}
}
else if (!vterm.containsBoundVar()){
// return true;
// cout<<"vterm and gterm"<<vterm << " # " <<gterm<<endl;
if(simplifyExpr(vterm) == simplifyExpr(gterm)) {
return true;
}
else{
return false;
}
}
else if(false && isSysPred(vterm) && isSysPred(gterm)){
TRACE("quant syspred"," vterm, gterm ", vterm.toString()+" :|: ", gterm.toString());
TRACE("quant syspred"," simplified vterm, gterm ", simplifyExpr(vterm).toString()+" :|: ", simplifyExpr(gterm).toString());
FatalAssert(false, "should not be here in synmatch");
exit(3);
}
else{
if(canGetHead(vterm)){
Expr vhead = getHead(vterm);
TRACE("quant match", "head vterm:", getHead(vterm), "");
if(vterm.isAtomicFormula()){
if (canGetHead(gterm)) {
if ( vhead != getHead(gterm) ){
return false;
}
return matchChild(gterm, vterm, env);
// for(int i=vterm.arity()-1; i >= 0; i--){
// if (false == recSynMatch(gterm[i], vterm[i] , env))
// return false;
// }
// return true;
}
else{
return false;
}
}
if ( (canGetHead(gterm)) && vhead == getHead(gterm)){
// if(gterm.arity() != vterm.arity()){
// return false;
// }
// for(int i=vterm.arity()-1; i >= 0; i--){
// if (false == recSynMatch(gterm[i], vterm[i] , env)) {
// return false;
// }
// }
// return true;
return matchChild(gterm, vterm, env);
}
if(!*d_useEqu){
return false;
}
// cout<<"==============================="<<endl;
// cout<<gterm<<" # " <<vterm<<endl;
/*
{ //
// std::set<Expr> eq_set;
std::map<Expr,bool> eq_set;
eq_set.clear();
eq_set[gterm]=true;
std::queue<Expr> eq_queue;
ExprMap<CDList<Expr>* >::iterator iter = d_eq_list.find(gterm);
if(iter != d_eq_list.end()){
for(size_t len =0; len< iter->second->size(); len++){
eq_queue.push((*(iter->second))[len]);
}
int count =0;
while(eq_queue.size()>0){
count++;
const Expr& cur = eq_queue.front();
eq_queue.pop();
if(eq_set.find(cur) == eq_set.end()){
if(canGetHead(cur) && getHead(cur) == vhead){
// cout<<"VTERM: "<<vterm<<endl;
// cout<<"FOUND: "<<cur<<endl;
// cout<<"GTERM: "<<gterm<<endl;
// cout<<"--good match: " << count << " // " << gterm << " # " << cur << endl;
// cout<<"===good simple: " << count << " // " << simplifyExpr(gterm) << " # " << simplifyExpr(cur) << endl;
if(simplifyExpr(cur) != simplifyExpr(gterm)){
// return false;
// return matchChild(cur, vterm, env);
// cout<<"en? "<<gterm<<" # " <<cur <<" # " <<vterm<<endl;
}
else{
// cout<<"--good match: " << count << " // " << gterm << " # " << cur << endl;
// cout<<"===good simple: " << count << " // " << simplifyExpr(gterm) << " # " << simplifyExpr(cur) << endl;
// return matchChild(cur, vterm, env);
}
}
eq_set[cur]=true;
ExprMap<CDList<Expr>* >::iterator iter = d_eq_list.find(cur);
if(iter != d_eq_list.end()){
for(size_t len =0; len< iter->second->size(); len++){
eq_queue.push((*(iter->second))[len]);
}
}
}
}
}
// return false;
}
*/
if( d_same_head_expr.count(vhead) > 0 ) {
const Expr& findGterm = simplifyExpr(gterm);
//if(isIntx(findGterm,0) || isIntx(findGterm,1)) return false;//special for simplify benchmark
TRACE("quant match", "find gterm:", findGterm.toString(),"");
CDList<Expr>* gls = d_same_head_expr[vhead];
/*
{ int count =0;
for(size_t i = 0; i<gls->size(); i++){
if (simplifyExpr((*gls)[i]) == findGterm){
count++;
}
}
if(count>1){
cout<<"count " << count << " # " << gls->size() << " | "<<gterm<<endl;
for(size_t i = 0; i<gls->size(); i++){
if (simplifyExpr((*gls)[i]) == findGterm){
cout<<"eq "<<(*gls)[i]<<endl;
}
}
}
}
*/
for(size_t i = 0; i<gls->size(); i++){
if (simplifyExpr((*gls)[i]) == findGterm){
TRACE("quant match", "find matched gterm:", (*gls)[i].toString(),"");
DebugAssert((*gls)[i].arity() == vterm.arity(), "gls has different arity");
const Expr& newgterm = (*gls)[i];
for(int child=vterm.arity()-1; child >= 0 ; child--){
if (false == recSynMatch(newgterm[child], vterm[child] , env)){
TRACE("quant match", "match false", (*gls)[i][child].toString(), vterm[child].toString());
return false;
}
}
TRACE("quant match", "good match, return true:", gterm, vterm.toString());
// cout<<"quant good match: " <<i<<" // "<<gterm << " # "<<vterm<<endl;
// cout<<"quant simple: " <<i<<" // "<<simplifyExpr(gterm) << " # "<<vterm<<endl;
return true;
}
}//end of for
return false;
}
else {
return false;//end of if
}
}
else{
TRACE("quant match more", "match more", gterm.toString()+" # ", vterm.toString());
if( (gterm.getKind() == vterm.getKind()) &&
(gterm.arity() == vterm.arity()) &&
gterm.arity()>0 ){
// for(int child=0; child < vterm.arity() ; child++){
// if (false == recSynMatch(gterm[child], vterm[child] , env)){
// TRACE("quant match", "match false", gterm[child].toString(), vterm[child].toString());
// return false;
// }
// }
// return true;
// if( gterm.getKind() == PLUS || gterm.getKind() == MINUS){
// cout<<"g v"<<gterm<< " # " <<vterm<<endl;
// }
return matchChild(gterm, vterm, env);
}
else {
// if( gterm.getKind() == PLUS || gterm.getKind() == MINUS){
// static bool gvfound = false;
// if(!gvfound){
// cout<<"g v 1"<<endl;
// gvfound =true;
// }
//gterm<< " # " <<vterm<<endl;
// }
return false;
}
}
}
}
/*
bool TheoryQuant::synMatchTopPred(const Expr& gterm, Trigger trig, ExprMap<Expr>& env){
const Expr vterm = trig.getEx();
TRACE("quant toppred", "top pred: gterm:| "+gterm.toString()," vterm:| "+vterm.toString(),"");
DebugAssert ((BOUND_VAR != gterm.getKind()),"gound term "+gterm.toString()+" has bound var");
DebugAssert ((BOUND_VAR != vterm.getKind()),"top pred match "+gterm.toString()+" has bound var");
if(gterm.isEq() || vterm.isEq()){
return false; // we do not match with equality
}
bool res2=false;
// if(vterm.arity() != gterm.arity()) return false;
if(trig.isSimp()){
if(trig.getHead() == getHead(gterm) ){
for(int i = vterm.arity()-1; i>=0 ; i--){
if(BOUND_VAR != vterm[i].getKind()){
if(simplifyExpr(gterm[i]) != simplifyExpr(vterm[i])) {
return false;
}
}
}
for(int i = vterm.arity()-1; i>=0 ; i--){
if(BOUND_VAR == vterm[i].getKind()){
if(d_allout){
env[vterm[i]] = simplifyExpr(gterm[i]);
}
else {
env[vterm[i]] = simplifyExpr(gterm[i]);
}
}
}
return true;
}
else{
return false;
}
}
if(!(isSysPred(vterm) && isSysPred(gterm))){
if(isSysPred(vterm) || isSysPred(gterm)) {
return false;
}
if(!usefulInMatch(gterm)){
return false;
}
if(trig.getHead() != getHead(gterm)){
return false;
}
if(!gterm.getType().isBool()){
res2= recSynMatch(gterm, vterm, env);
return res2;
}
if(!*d_usePolarity){
return recSynMatch(gterm, vterm, env);
}
const bool gtrue = (trueExpr()==findExpr(gterm));
if(gtrue ){
if(trig.isNeg()) {
return recSynMatch(gterm, vterm, env);
}
else{
return false;
}
}
const bool gfalse = (falseExpr()==findExpr(gterm));
if(gfalse){
if (trig.isPos()){
return recSynMatch(gterm, vterm, env);
}
else{
return false;
}
}
else {
return false;
}
}
else{
DebugAssert((2==gterm.arity() && 2==vterm.arity()), "impossible situation in top pred");
DebugAssert(!((isLE(gterm) || isLT(gterm)) && !isIntx(gterm[0],0)), "canonical form changed");
#ifdef DEBUG
if( CVC3::debugger.trace("quant toppred") ){
cout << "toppred gterm, vterm" << gterm << "::" << vterm << endl;
cout << findExpr(gterm) << "::" << trig.isPos() << "|" << trig.isNeg() << endl;
}
#endif
Expr gl = getLeft(gterm[1]);
Expr gr = getRight(gterm[1]);
if(null_expr == gr || null_expr == gl){
gl = gterm[0];
gr = gterm[1];
}
Expr vr, vl;
Expr tvr, tvl;
tvr=null_expr;
tvl=null_expr;
if(isGE(vterm) || isGT(vterm)){
vr = vterm[0];
vl = vterm[1];
}
else if(isLE(vterm) || isLT(vterm)){
vr = vterm[1];
vl = vterm[0];
}
else{
DebugAssert(false, "impossilbe in toppred");
}
if(isIntx(vl,0)){
tvl = getLeft(vr);
tvr = getRight(vr);
}
else if(isIntx(vr,0)) {
tvl = getLeft(vl);
tvr = getRight(vl);
}
if( (null_expr != tvl) && (null_expr != tvr)){
vl = tvl;
vr = tvr;
}
const bool gtrue = (trueExpr()==findExpr(gterm));
const bool gfalse = (falseExpr()==findExpr(gterm));
TRACE("quant toppred"," vl, gl, vr, gr:", vl.toString()+"::"+gl.toString()+"||", vr.toString()+"::"+gr.toString());
bool res;
DebugAssert(!(trig.isNeg() && trig.isPos()), "expr in both pos and neg");
if(!*d_usePolarity){
return (recSynMatch(gl, vl, env) && recSynMatch(gr, vr, env));
}
if(trig.isNeg()){
if (( gtrue ) ) {
res=(recSynMatch(gl, vl, env) && recSynMatch(gr, vr, env));
}
else {
res=(recSynMatch(gl, vr, env) && recSynMatch(gr, vl, env));
}
}
else if(trig.isPos()){
if (( gfalse )) {
res=(recSynMatch(gl, vl, env) && recSynMatch(gr, vr, env));
}
else {
res=(recSynMatch(gl, vr, env) && recSynMatch(gr, vl, env));
}
}
else {
DebugAssert(false, "impossible polarity for trig");
res = false;
}
#ifdef DEBUG
if( CVC3::debugger.trace("quant toppred") ){
cout<<"res| "<< res << " | " << gtrue << " | " << gfalse << endl;
}
#endif
return res;
}
}
bool TheoryQuant::recSynMatch(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env){
TRACE("quant match", "gterm:| "+gterm.toString()," vterm:| "+vterm.toString(),"");
DebugAssert ((BOUND_VAR != gterm.getKind()),"gound term "+gterm.toString()+" has bound var");
if (BOUND_VAR == vterm.getKind()) {
TRACE("quant match", "bound var found;", vterm.toString(),"");
ExprMap<Expr>::iterator p = env.find(vterm);
if ( p != env.end()){
if (simplifyExpr(gterm) != simplifyExpr(p->second)){
return false;
}
else
return true;
}
else {
env[vterm] = simplifyExpr(gterm);
return true;
}
}
else if (!vterm.containsBoundVar()){
if(simplifyExpr(vterm) == simplifyExpr(gterm)) {
return true;
}
else{
return false;
}
}
else if(false && isSysPred(vterm) && isSysPred(gterm)){
TRACE("quant syspred"," vterm, gterm ", vterm.toString()+" :|: ", gterm.toString());
TRACE("quant syspred"," simplified vterm, gterm ", simplifyExpr(vterm).toString()+" :|: ", simplifyExpr(gterm).toString());
FatalAssert(false, "should not be here in synmatch");
exit(3);
}
else{
if(canGetHead(vterm)){
Expr vhead = getHead(vterm);
TRACE("quant match", "head vterm:", getHead(vterm), "");
if(vterm.isAtomicFormula()){
if (canGetHead(gterm)) {
if ( vhead != getHead(gterm) ){
return false;
}
for(int i=vterm.arity()-1; i >= 0; i--){
if (false == recSynMatch(gterm[i], vterm[i] , env))
return false;
}
return true;
}
else{
return false;
}
}
if ( (canGetHead(gterm)) && vhead == getHead(gterm)){
if(gterm.arity() != vterm.arity()){
return false;
}
for(int i=vterm.arity()-1; i >= 0; i--){
if (false == recSynMatch(gterm[i], vterm[i] , env)) {
return false;
}
}
return true;
}
if(false && !*d_useEqu){
return false;
}
if( d_same_head_expr.count(vhead) > 0 ) {
const Expr& findGterm = simplifyExpr(gterm);
//if(isIntx(findGterm,0) || isIntx(findGterm,1)) return false;//special for simplify benchmark
TRACE("quant match", "find gterm:", findGterm.toString(),"");
CDList<Expr>* gls = d_same_head_expr[vhead];
for(size_t i = 0; i<gls->size(); i++){
if (simplifyExpr((*gls)[i]) == findGterm){
TRACE("quant match", "find matched gterm:", (*gls)[i].toString(),"");
DebugAssert((*gls)[i].arity() == vterm.arity(), "gls has different arity");
for(int child=vterm.arity()-1; child >= 0 ; child--){
const Expr& newgterm = (*gls)[i];
if (false == recSynMatch(newgterm[child], vterm[child] , env)){
TRACE("quant match", "match false", (*gls)[i][child].toString(), vterm[child].toString());
return false;
}
}
TRACE("quant match", "good match, return true:", gterm, vterm.toString());
return true;
}
}//end of for
return false;
}
else {
return false;//end of if
}
}
else{
TRACE("quant match more", "match more", gterm.toString()+" # ", vterm.toString());
if( (gterm.getKind() == vterm.getKind()) &&
(gterm.arity() == vterm.arity()) &&
gterm.arity()>0 ){
for(int child=0; child < vterm.arity() ; child++){
if (false == recSynMatch(gterm[child], vterm[child] , env)){
TRACE("quant match", "match false", gterm[child].toString(), vterm[child].toString());
return false;
}
}
return true;
}
else return false;
}
}
}
*/
void TheoryQuant::goodSynMatch(const Expr& e,
const std::vector<Expr> & boundVars,
std::vector<std::vector<Expr> >& instBinds,
std::vector<Expr>& instGterms,
const CDList<Expr>& allterms,
size_t tBegin){
for (size_t i=tBegin; i<allterms.size(); i++) {
Expr gterm = allterms[i];
if (0 == gterm.arity() )
continue;
TRACE("quant matching", gterm.toString(), "||", e.toString()) ;
// if( usefulInMatch(gterm) && possibleMatch(gterm,e)) {
if(usefulInMatch(gterm)) {
ExprMap<Expr> env;
env.clear();
bool found = recSynMatch(gterm,e,env);
if(found){
TRACE("quant matching found", " good:",gterm.toString()+" to " , e.toString());
TRACE("quant matching found", " simplified good:",simplifyExpr(gterm).toString()+" to " , simplifyExpr(e).toString());
std::vector<Expr> inst;
DebugAssert((boundVars.size() == env.size()),"bound var size != env.size()");
for(size_t i=0; i<boundVars.size(); i++) {
ExprMap<Expr>::iterator p = env.find(boundVars[i]);
DebugAssert((p!=env.end()),"bound var cannot be found");
inst.push_back(p->second);
}
instBinds.push_back(inst);
instGterms.push_back(gterm);
}
else{
TRACE("quant matching", "bad one",gterm.toString()+" to " , e.toString());
}
}
}
}
/*
void TheoryQuant::goodSynMatchNewTrig(const Trigger& trig,
const std::vector<Expr> & boundVars,
std::vector<std::vector<Expr> >& instBinds,
std::vector<Expr>& instGterms,
const CDList<Expr>& allterms,
size_t tBegin){
for (size_t i=tBegin; i<allterms.size(); i++) {
Expr gterm (allterms[i]);
// TRACE("quant matching", gterm.toString(), "||", trig.getEx().toString()) ;
if(usefulInMatch(gterm)) {
ExprMap<Expr> env;
env.clear();
bool found = synMatchTopPred(gterm,trig,env);
if(found){
//TRACE("quant matching found", " top good:",gterm.toString()+" to " , trig.getEx().toString());
std::vector<Expr> inst;
inst.clear();
DebugAssert((boundVars.size() <= env.size()),"bound var size != env.size()");
for(size_t i=0; i<boundVars.size(); i++) {
ExprMap<Expr>::iterator p = env.find(boundVars[i]);
DebugAssert((p!=env.end()),"bound var cannot be found");
inst.push_back(p->second);
}
instBinds.push_back(inst);
instGterms.push_back(gterm);
}
else{
// TRACE("quant matching", "bad one",gterm.toString()+" to ", trig.getEx().toString());
}
}
}
}
*/
/*
bool TheoryQuant::hasGoodSynInstNewTrigOld(Trigger& trig,
std::vector<Expr> & boundVars,
std::vector<std::vector<Expr> >& instBinds,
std::vector<Expr>& instGterms,
const CDList<Expr>& allterms,
size_t tBegin){
const std::set<Expr>& bvs = getBoundVars(trig.getEx());
boundVars.clear();
for(std::set<Expr>::const_iterator i=bvs.begin(),iend=bvs.end(); i!=iend; ++i)
boundVars.push_back(*i);
instBinds.clear();
goodSynMatchNewTrig(trig, boundVars, instBinds, instGterms, allterms, tBegin);
if (instBinds.size() > 0)
return true;
else
return false;
}
bool TheoryQuant::hasGoodSynInstNewTrig(Trigger& trig,
const std::vector<Expr>& boundVars,
std::vector<std::vector<Expr> >& instBinds,
std::vector<Expr>& instGterms,
const CDList<Expr>& allterms,
size_t tBegin){
// boundVars=trig.getBVs();
// const std::set<Expr>& bvs = getBoundVars(trig.getEx());
// boundVars.clear();
// for(std::set<Expr>::const_iterator i=bvs.begin(),iend=bvs.end(); i!=iend; ++i)
// boundVars.push_back(*i);
instBinds.clear();
goodSynMatchNewTrig(trig, boundVars, instBinds, instGterms, allterms, tBegin);
if (instBinds.size() > 0)
return true;
else
return false;
}
*/
int TheoryQuant::loc_gterm(const std::vector<Expr>& border,
const Expr& vterm,
int pos){
const std::vector<Expr>& order = d_mtrigs_bvorder[vterm];
const Expr& var = order[pos];
for(size_t i=0; i<border.size(); i++){
if (border[i] == var) return i;
}
DebugAssert(false, "internal error in loc_germ");
return -1;
}
void TheoryQuant::recSearchCover(const std::vector<Expr>& border,
const std::vector<Expr>& mtrigs,
int cur_depth,
std::vector<std::vector<Expr> >& instSet,
std::vector<Expr>& cur_inst
){
int max_dep = mtrigs.size();
if(cur_depth >= max_dep) return;
Expr cur_vterm = mtrigs[cur_depth]; //get the current vterm
if(d_mtrigs_inst.count(cur_vterm) <=0) return;
CDList<std::vector<Expr> >* gterm_list = d_mtrigs_inst[cur_vterm]; // get the list of ground term found for cur_vterm
for(size_t i=0; i< gterm_list->size(); i++){
const std::vector<Expr>& cur_gterm = (*gterm_list)[i];
std::vector<Expr> new_inst(border.size()); //get a new inst array
for(size_t j=0; j< border.size(); j++){
new_inst[j]=cur_inst[j]; //copy to cur_int to new_inst
}
bool has_problem = false;//next, try to put the cur gterm into new_inst
for(size_t j=0; j< cur_gterm.size(); j++){
int cur_loc_gterm = loc_gterm(border, cur_vterm, j);
if( null_expr == new_inst[cur_loc_gterm]){
new_inst[cur_loc_gterm] = cur_gterm[j];
}
else if (new_inst[cur_loc_gterm] != cur_gterm[j]){
has_problem = true;
break;
}
}
if (has_problem){
continue;
}
bool finished = true;
for(size_t j=0; j< border.size() ;j++){
if(null_expr == new_inst[j]){
finished = false;
break;
}
}
if(finished){
std::vector<Expr> good_inst;
for(size_t j=0; j<border.size(); j++){
good_inst.push_back(new_inst[j]);
}
instSet.push_back(good_inst);
}
else{
recSearchCover(border,
mtrigs,
cur_depth+1,
instSet,
new_inst);
}
}//end of for
}
void TheoryQuant::searchCover(const Expr& thm,
const std::vector<Expr>& border,
std::vector<std::vector<Expr> >& instSet
){
std::vector<Expr> dumy(border.size()) ; //use dynamic array here
for(size_t j=0; j< border.size() ;j++){
dumy[j]=null_expr;
}
const std::vector<Expr>& mtrigs = d_multTriggers[thm];
recSearchCover(border, mtrigs, 0, instSet, dumy);
}
bool TheoryQuant::hasGoodSynMultiInst(const Expr& thm,
std::vector<Expr> & boundVars,
std::vector<std::vector<Expr> >& instSet,
const CDList<Expr>& allterms,
size_t tBegin){
const std::set<Expr>& bvs = getBoundVars(thm);
boundVars.clear();
for(std::set<Expr>::const_iterator i=bvs.begin(),iend=bvs.end(); i!=iend; ++i)
boundVars.push_back(*i);
instSet.clear();
bool new_match = false;
//assumption: every trig is different
//this is not true later, fix this asap
const std::vector<Expr>& mtrigs = d_multTriggers[thm];
for(std::vector<Expr>::const_iterator i= mtrigs.begin(), iend = mtrigs.end(); i != iend; i++){
if(d_mtrigs_bvorder[*i].empty()){ //setup an order
const std::set<Expr>& trig_bvs = getBoundVars(*i);
for(std::set<Expr>::const_iterator j= trig_bvs.begin(), jend = trig_bvs.end();
j != jend;
j++){
d_mtrigs_bvorder[*i].push_back(*j);
}
}
const std::vector<Expr>& trig_bvorder = d_mtrigs_bvorder[*i];
// std::set<std::vector<Expr> > trig_insts;
std::vector<std::vector<Expr> > trig_insts;
trig_insts.clear();
std::vector<Expr> gtms;
goodSynMatch(*i, trig_bvorder, trig_insts, gtms, allterms, tBegin);
if (trig_insts.size() > 0){
new_match=true;
if(d_mtrigs_inst.count(*i) <= 0){
d_mtrigs_inst[*i] = new(true) CDList<std::vector<Expr> > (theoryCore()->getCM()->getCurrentContext());
}
for(std::vector<std::vector<Expr> >::const_iterator j = trig_insts.begin(), jend = trig_insts.end();
j != jend;
j++){
d_mtrigs_inst[*i]->push_back(*j);
for(std::vector<Expr>::const_iterator k = j->begin(), kend = j->end();
k != kend;
k++){
}
}
}
} // end of for
for(std::vector<Expr>::const_iterator i= mtrigs.begin(), iend = mtrigs.end(); i != iend; i++){
if (d_mtrigs_inst.count(*i) <=0 ) continue;
for(CDList<std::vector<Expr> >::const_iterator j = d_mtrigs_inst[*i]->begin(),
jend = d_mtrigs_inst[*i]->end();
j != jend;
j++){
for(std::vector<Expr>::const_iterator k = j->begin(), kend = j->end();
k != kend;
k++){
}
}
}
{//code for search a cover
if(new_match){
searchCover(thm, boundVars, instSet);
}
}
if(instSet.size() > 0 ) {
return true;
}
else {
return false;
}
}
bool inStrCache(std::set<std::string> cache, std::string str){
return (cache.find(str) != cache.end());
}
bool TheoryQuant::hasGoodSemInst(const Expr& e,
std::vector<Expr> & boundVars,
std::set<std::vector<Expr> >& instSet,
size_t tBegin){
return false;
}
void genPartInstSetThm(const std::vector<Expr>& bVarsThm,
std::vector<Expr>& bVarsTerm,
const std::vector<std::vector<Expr> >& termInst,
std::vector<std::vector<Expr> >& instSetThm){
ExprMap<bool> bVmap;
for(size_t i=0; i< bVarsThm.size(); ++i) {
bVmap[bVarsThm[i]]=true;
}
std::vector<Expr> tempBVterm;
std::vector<int> locTerm;
for (size_t j=0; j<bVarsTerm.size(); j++){
if (bVmap.count(bVarsTerm[j]) > 0){
locTerm.push_back(1);
tempBVterm.push_back(bVarsTerm[j]);
}
else{
locTerm.push_back(0);
}
}
DebugAssert(locTerm.size() == bVarsTerm.size(), "locTerm.size !- bVarsTerm.size()");
for(std::vector<std::vector<Expr> >::const_iterator i=termInst.begin(),
iend=termInst.end();i!=iend; i++) {
std::vector<Expr> buf;
buf.clear();
for(size_t j=0; j< bVarsTerm.size(); ++j){
if(locTerm[j])
buf.push_back((*i)[j]);
}
instSetThm.push_back(buf);
}
bVarsTerm=tempBVterm;
}
void genInstSetThm(const std::vector<Expr>& bVarsThm,
const std::vector<Expr>& bVarsTerm,
const std::vector<std::vector<Expr> >& termInst,
std::vector<std::vector<Expr> >& instSetThm){
std::vector<int> bVmap;
for(size_t i=0; i< bVarsThm.size(); ++i) {
bVmap.push_back(-1);
for (size_t j=0; j<bVarsTerm.size(); j++){
if (bVarsThm[i] == bVarsTerm[j]){
DebugAssert(bVmap[i] == -1, "bVmap[1] != -1");
bVmap[i]=j;
}
}
}
for(size_t i=0; i< bVarsThm.size(); ++i)
if( -1 == bVmap[i]) {
return;
}
for(std::vector<std::vector<Expr> >::const_iterator i=termInst.begin(),
iend=termInst.end();i!=iend; i++) {
std::vector<Expr> buf;
buf.clear();
for(size_t j=0; j< bVarsThm.size(); ++j){
buf.push_back((*i)[bVmap[j]]);
}
instSetThm.push_back(buf);
}
}
/*
void TheoryQuant::synInst(const Theorem & univ, const CDList<Expr>& allterms, size_t tBegin ){
if(d_useFullTrig){
synFullInst(univ, allterms, tBegin);
}
if(d_useMultTrig){
synMultInst(univ, allterms, tBegin);
}
if(d_usePartTrig){
synPartInst(univ, allterms, tBegin);
}
}
*/
inline bool TheoryQuant::transFound(const Expr& comb){
return (d_trans_found.count(comb) > 0);
}
inline void TheoryQuant::setTransFound(const Expr& comb){
d_trans_found[comb] = true;
}
inline bool TheoryQuant::trans2Found(const Expr& comb){
return (d_trans2_found.count(comb) > 0);
}
inline void TheoryQuant::setTrans2Found(const Expr& comb){
d_trans2_found[comb] = true;
}
inline CDList<Expr> & TheoryQuant::backList(const Expr& ex){
if(d_trans_back.count(ex)>0){
return *d_trans_back[ex];
}
else{
return null_cdlist;
}
}
inline CDList<Expr> & TheoryQuant::forwList(const Expr& ex){
if(d_trans_forw.count(ex)>0){
return *d_trans_forw[ex];
}
else{
return null_cdlist;
}
}
inline void TheoryQuant::pushBackList(const Expr& node, Expr ex){
if(d_trans_back.count(node)>0){
d_trans_back[node]->push_back(ex);
}
else{
d_trans_back[node] = new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext());
d_trans_back[node]->push_back(ex);
}
}
inline void TheoryQuant::pushForwList(const Expr& node, Expr ex){
if(d_trans_forw.count(node)>0){
d_trans_forw[node]->push_back(ex);
}
else{
d_trans_forw[node] = new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext());
d_trans_forw[node]->push_back(ex);
}
}
/*
void TheoryQuant::synFullInst(const Theorem & univ, const CDList<Expr>& allterms, size_t tBegin ){
const Expr& quantExpr = univ.getExpr();
// const std::vector<Expr>& bVarsThm = quantExpr.getVars();
std::vector<Expr> bVarsThm = quantExpr.getVars();
TRACE("quant inst", "try full inst with:|", quantExpr.toString() , " ");
std::vector<std::vector<Expr> > instBindsThm; //set of instantiations for the thm,
std::vector<std::vector<Expr> > instBindsTerm; //bindings, in the order of bVarsTrig
std::vector<Expr > instGterms; //instGterms are gterms matched, instBindsTerm and instGterms must have the same length
std::vector<Expr> bVarsTrig;
if(*d_useTrigNew){
std::vector<Trigger>& new_trigs=d_fullTrigs[quantExpr];
for( size_t i= 0; i<new_trigs.size(); i++) {
Trigger& trig = new_trigs[i];
// if( 0 != trig.getPri()) continue;
TRACE("quant inst","try new full trigger:|", trig.getEx().toString(),"");
instBindsTerm.clear();
bVarsTrig.clear();
instBindsThm.clear();
instGterms.clear();
{//code for trans2
if(trig.hasTr2()){
//if(hasGoodSynInstNewTrig(trig, bVarsTrig, instBindsTerm, instGterms, allterms, tBegin)) {
if(hasGoodSynInstNewTrig(trig, trig.getBVs(), instBindsTerm, instGterms, allterms, tBegin)) {
for(size_t j=0; j<instBindsTerm.size(); j++){
DebugAssert(2 == instBindsTerm[j].size(), "internal error in trans2");
Expr& gterm = instGterms[j];
if(simplifyExpr(instBindsTerm[j][0]) != simplifyExpr(instBindsTerm[j][1])){
Expr comb = Expr(RAW_LIST,instBindsTerm[j][0],instBindsTerm[j][1]);
if(!trans2Found(comb)){
setTrans2Found(comb);
TRACE("quant trans","new trans2: ", vectorExpr2string(instBindsTerm[j]), "");
Expr comb_rev = Expr(RAW_LIST,instBindsTerm[j][1],instBindsTerm[j][0]);
if(trans2Found(comb_rev)){
Expr sr(instBindsTerm[j][0]);
Expr dt(instBindsTerm[j][1]);
vector<Expr> bind;
bind.clear();
bind.push_back(sr);
bind.push_back(dt);
enqueueInst(univ, bind, gterm);
TRACE("quant inst", "trans pred rule2 ", univ.toString(), " | with bind: "+vectorExpr2string(bind)); TRACE("quant trans", "trans2 ", vectorExpr2string(bind), "");
}
}
}
}
}
return;
}
}
{//code for trans pred
if(trig.hasTr()){
// if(hasGoodSynInstNewTrig(trig, bVarsTrig, instBindsTerm, instGterms, allterms, tBegin)) {
if(hasGoodSynInstNewTrig(trig, trig.getBVs(), instBindsTerm, instGterms, allterms, tBegin)) {
for(size_t j=0; j<instBindsTerm.size(); j++){
DebugAssert(2 == instBindsTerm[j].size(), "internal error in trans");
Expr& gterm = instGterms[j];
if(simplifyExpr(instBindsTerm[j][0]) != simplifyExpr(instBindsTerm[j][1])){
Expr comb = Expr(RAW_LIST,instBindsTerm[j][0],instBindsTerm[j][1]);
if(!transFound(comb)){
setTransFound(comb);
TRACE("quant trans","new: ", vectorExpr2string(instBindsTerm[j]), "");
Expr sr(instBindsTerm[j][0]);
Expr dt(instBindsTerm[j][1]);
const CDList<Expr>& dtForw = forwList(dt);
const CDList<Expr>& srBack = backList(sr);
for(size_t k=0; k<dtForw.size(); k++){
vector<Expr> bind;
bind.clear();
bind.push_back(sr);
bind.push_back(dt);
bind.push_back(dtForw[k]);
enqueueInst(univ, bind, gterm);
TRACE("quant inst", "trans pred rule", univ.toString(), " | with bind: "+vectorExpr2string(bind));
TRACE("quant trans", "trans res forw: ", vectorExpr2string(bind), "");
}
for(size_t k=0; k<srBack.size(); k++){
vector<Expr> bind;
bind.clear();
bind.push_back(srBack[k]);
bind.push_back(sr);
bind.push_back(dt);
enqueueInst(univ, bind, gterm);
TRACE("quant inst", "trans pred rule ", univ.toString(), " | with bind: "+vectorExpr2string(bind));
TRACE("quant trans", "trans res back: ", vectorExpr2string(bind), "");
}
pushForwList(sr,dt);
pushBackList(dt,sr);
}
}
}
}
return;
}
}
bool univsHasMoreBVs ;
univsHasMoreBVs = (d_hasMoreBVs.count(quantExpr) > 0);
// if ( !d_allout || !trig.isSimp() || univsHasMoreBVs || *d_useLazyInst){
// if ( !d_allout || !trig.isSimp() || univsHasMoreBVs || true){
if ( !d_allout || !trig.isSuperSimp() || univsHasMoreBVs ){
// if ( !d_allout || !trig.isSimp() || univsHasMoreBVs ){
*/
/*
if(hasGoodSynInstNewTrigOld(trig, bVarsTrig, instBindsTerm, instGterms, allterms, tBegin)) {
genInstSetThm(bVarsThm, bVarsTrig, instBindsTerm, instBindsThm);
for (size_t j = 0; j<instBindsTerm.size(); j++){
const Expr& gterm = instGterms[j];
const std::vector<Expr>& binds = instBindsThm[j];
enqueueInst(univ, trig, binds, gterm);
TRACE("quant inst", "insert full inst", univ.toString(), " | with bind: "+vectorExpr2string(binds));
}
}
*/
/*
bVarsTrig=trig.getBVs();//vVarsTrig is used later, do not forget this.
if(hasGoodSynInstNewTrig(trig, bVarsThm, instBindsTerm, instGterms, allterms, tBegin)) {
for (size_t j = 0; j<instBindsTerm.size(); j++){
const Expr& gterm = instGterms[j];
const std::vector<Expr>& binds = instBindsTerm[j];
enqueueInst(univ, trig, binds, gterm);
TRACE("quant inst", "insert full inst", univ.toString(), " | with bind: "+vectorExpr2string(binds));
}
}
}
// if(!d_allout || *d_useLazyInst){
if(!d_allout){
if(trig.hasRW() ){
if(1 == bVarsTrig.size()){
std::vector<Expr> tp = d_arrayIndic[trig.getHead()];
for(size_t i=0; i<tp.size(); i++){
std::vector<Expr> tp = d_arrayIndic[trig.getHead()];
Expr index = tp[i];
std::vector<Expr> temp;
temp.clear();
temp.push_back(index);
enqueueInst(univ, temp, index);
TRACE("quant inst", "read write rule", univ.toString(), " | with bind: "+vectorExpr2string(temp));
}
}
else{
}
}
}
}//end for each trigger
}
}
*/
void TheoryQuant::arrayHeuristic(const Trigger& trig, size_t univ_id){
std::vector<Expr> tp = d_arrayIndic[trig.head];
for(size_t i=0; i<tp.size(); i++){
const Expr& index = tp[i];
std::vector<Expr> temp;
temp.push_back(index);
enqueueInst(univ_id, temp, index);
// TRACE("quant inst", "read write rule", univ.toString(), " | with bind: "+vectorExpr2string(temp));
}
}
void TheoryQuant::synNewInst(size_t univ_id, const vector<Expr>& bind, const Expr& gterm, const Trigger& trig ){
if(trig.isMulti){
const multTrigsInfo& mtriginfo = d_all_multTrigsInfo[trig.multiId];
vector<Expr> actual_bind;
for(size_t i=0, iend=bind.size(); i<iend; i++){
if(null_expr != bind[i]){
actual_bind.push_back(bind[i]);
}
}
Expr actual_bind_expr = Expr(RAW_LIST, actual_bind);
size_t index = trig.multiIndex;
CDMap<Expr,bool> * cur_cd_map = mtriginfo.var_binds_found[index];
CDMap<Expr,bool>::iterator cur_iter = cur_cd_map->find(actual_bind_expr);
if (cur_cd_map->end() != cur_iter){
return;
}
(*cur_cd_map)[actual_bind_expr] = true;
const vector<size_t>& comm_pos = mtriginfo.common_pos[0];
size_t comm_pos_size = comm_pos.size();
Expr comm_expr;
vector<Expr> comm_expr_vec;
for(size_t i = 0; i < comm_pos_size; i++){
comm_expr_vec.push_back(bind[comm_pos[i]]);
// cout<<"bind " <<bind[comm_pos[i]]<<endl;
}
if(0 == comm_pos_size){
comm_expr = null_expr;
}
else{
comm_expr = Expr(RAW_LIST, comm_expr_vec);
}
Expr uncomm_expr;
vector<Expr> uncomm_expr_vec;
const vector<size_t>& uncomm_pos = mtriginfo.var_pos[index];
size_t uncomm_pos_size = uncomm_pos.size();
for(size_t i = 0; i< uncomm_pos_size; i++){
uncomm_expr_vec.push_back(bind[uncomm_pos[i]]);
}
uncomm_expr = Expr(RAW_LIST, uncomm_expr_vec);
CDList<Expr>* add_into_list ;
CDList<Expr>* iter_list;
ExprMap<CDList<Expr>* >::iterator add_into_iter;
ExprMap<CDList<Expr>* >::iterator iter_iter;
size_t other_index = 0;
if(0 == index){
other_index =1;
}
else if (1 == index){
other_index = 0;
}
else{
FatalAssert(false, "wrong ");
}
// cout<<"comm expr"<<comm_expr<<endl;
add_into_iter = mtriginfo.uncomm_list[index]->find(comm_expr);
iter_iter = mtriginfo.uncomm_list[other_index]->find(comm_expr);
if(mtriginfo.uncomm_list[index]->end() == add_into_iter){
add_into_list = new (true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext());
(*mtriginfo.uncomm_list[index])[comm_expr] = add_into_list;
}
else{
add_into_list = add_into_iter->second;
}
// cout<<"uncomm expr"<<uncomm_expr<<endl;
add_into_list->push_back(uncomm_expr);
if(mtriginfo.uncomm_list[other_index]->end() == iter_iter){
return;
}
else{
iter_list = iter_iter->second;
}
const vector<size_t>& uncomm_iter_pos = mtriginfo.var_pos[other_index];
size_t uncomm_iter_pos_size = uncomm_iter_pos.size();
for(size_t i =0, iend = iter_list->size(); i<iend; i++){
const Expr& cur_iter_expr = (*iter_list)[i];
vector<Expr> new_bind(bind);
for(size_t j=0; j<uncomm_iter_pos_size; j++){
new_bind[uncomm_iter_pos[j]] = cur_iter_expr[j];
}
enqueueInst(univ_id, new_bind, gterm);
}
return;
}
// cout<<"synnewinst "<<univ_id<<endl;
{//code for trans2
if(trig.hasT2){
vector<Expr> actual_bind;
for(size_t i=0; i<bind.size(); i++){
if(bind[i] != null_expr){
actual_bind.push_back(bind[i]);
}
}
if(actual_bind.size() != 2){
cout<<"2 != bind.size()" <<endl;
}
Expr acb1 = simplifyExpr(actual_bind[0]);
Expr acb2 = simplifyExpr(actual_bind[1]);
actual_bind[0]=acb1;
actual_bind[1]=acb2;
if(acb1 != acb2){
Expr comb = Expr(RAW_LIST,acb1, acb2);
if(!trans2Found(comb)){
setTrans2Found(comb);
Expr comb_rev = Expr(RAW_LIST,acb2, acb1);
if(trans2Found(comb_rev)){
enqueueInst(univ_id, actual_bind, gterm);
}
}
}
return;
}
}
{//code for trans pred
if(trig.hasTrans){
vector<Expr> actual_bind;
for(size_t i=0; i<bind.size(); i++){
if(bind[i] != null_expr){
actual_bind.push_back(simplifyExpr(bind[i]));
}
}
if(simplifyExpr(actual_bind[0]) != simplifyExpr(actual_bind[1])){
Expr comb = Expr(RAW_LIST,actual_bind[0], actual_bind[1]);
if(!transFound(comb)){
setTransFound(comb);
Expr sr(actual_bind[0]);
Expr dt(actual_bind[1]);
const CDList<Expr>& dtForw = forwList(dt);
const CDList<Expr>& srBack = backList(sr);
for(size_t k=0; k<dtForw.size(); k++){
vector<Expr> tri_bind;
tri_bind.push_back(sr);
tri_bind.push_back(dt);
tri_bind.push_back(dtForw[k]);
enqueueInst(univ_id, tri_bind, gterm);
}
for(size_t k=0; k<srBack.size(); k++){
vector<Expr> tri_bind;
tri_bind.push_back(srBack[k]);
tri_bind.push_back(sr);
tri_bind.push_back(dt);
enqueueInst(univ_id, tri_bind, gterm);
// TRACE("quant inst", "trans pred rule ", univ.toString(), " | with bind: "+vectorExpr2string(bind));
// TRACE("quant trans", "trans res back: ", vectorExpr2string(bind), "");
}
pushForwList(sr,dt);
pushBackList(dt,sr);
}
}
return;
}
}
// cout<<"before enqueueisnt"<<endl;
enqueueInst(univ_id, bind, gterm);
// if(!d_allout || *d_useLazyInst){
}
/*
void TheoryQuant::synNewInst(size_t univ_id, const vector<Expr>& bind, const Expr& gterm, const Trigger& trig ){
// cout<<"synnewinst "<<univ_id<<endl;
{//code for trans2
if(trig.hasT2){
vector<Expr> actual_bind;
for(size_t i=0; i<bind.size(); i++){
if(bind[i] != null_expr){
actual_bind.push_back(bind[i]);
}
}
if(actual_bind.size() != 2){
cout<<"2 != bind.size()" <<endl;
}
if(simplifyExpr(actual_bind[0]) != simplifyExpr(actual_bind[1])){
Expr comb = Expr(RAW_LIST,actual_bind[0], actual_bind[1]);
if(!trans2Found(comb)){
setTrans2Found(comb);
Expr comb_rev = Expr(RAW_LIST,actual_bind[1], actual_bind[0]);
if(trans2Found(comb_rev)){
enqueueInst(univ_id, actual_bind, gterm);
}
}
}
return;
}
}
{//code for trans pred
if(trig.hasTrans){
vector<Expr> actual_bind;
for(size_t i=0; i<bind.size(); i++){
if(bind[i] != null_expr){
actual_bind.push_back(bind[i]);
}
}
if(simplifyExpr(actual_bind[0]) != simplifyExpr(actual_bind[1])){
Expr comb = Expr(RAW_LIST,actual_bind[0], actual_bind[1]);
if(!transFound(comb)){
setTransFound(comb);
Expr sr(actual_bind[0]);
Expr dt(actual_bind[1]);
const CDList<Expr>& dtForw = forwList(dt);
const CDList<Expr>& srBack = backList(sr);
for(size_t k=0; k<dtForw.size(); k++){
vector<Expr> tri_bind;
tri_bind.push_back(sr);
tri_bind.push_back(dt);
tri_bind.push_back(dtForw[k]);
enqueueInst(univ_id, tri_bind, gterm);
}
for(size_t k=0; k<srBack.size(); k++){
vector<Expr> tri_bind;
tri_bind.push_back(srBack[k]);
tri_bind.push_back(sr);
tri_bind.push_back(dt);
enqueueInst(univ_id, tri_bind, gterm);
// TRACE("quant inst", "trans pred rule ", univ.toString(), " | with bind: "+vectorExpr2string(bind));
// TRACE("quant trans", "trans res back: ", vectorExpr2string(bind), "");
}
pushForwList(sr,dt);
pushBackList(dt,sr);
}
}
return;
}
}
// cout<<"before enqueueisnt"<<endl;
enqueueInst(univ_id, bind, gterm);
// if(!d_allout || *d_useLazyInst){
if(!d_allout){
if(trig.hasRWOp ){
if(1 == trig.bvs.size()){
std::vector<Expr> tp = d_arrayIndic[trig.head];
for(size_t i=0; i<tp.size(); i++){
std::vector<Expr> tp = d_arrayIndic[trig.head];
Expr index = tp[i];
std::vector<Expr> temp;
temp.clear();
temp.push_back(index);
enqueueInst(univ_id, temp, index);
// TRACE("quant inst", "read write rule", univ.toString(), " | with bind: "+vectorExpr2string(temp));
}
}
else{
}
}
}
}
*/
/*
void TheoryQuant::synMultInst(const Theorem & univ, const CDList<Expr>& allterms, size_t tBegin ){
const Expr& quantExpr = univ.getExpr();
if(d_multTriggers[quantExpr].size() <= 0) return ;
TRACE("quant inst", "try muli with:|", quantExpr.toString() , " ");
const std::vector<Expr>& bVarsThm = quantExpr.getVars();
std::vector<std::vector<Expr> > instSetThm; //set of instantiations for the thm
std::vector<std::vector<Expr> > termInst; //terminst are bindings, in the order of bVarsTrig
std::vector<Expr> bVarsTrig;
if(hasGoodSynMultiInst(quantExpr, bVarsTrig, termInst, allterms, tBegin)) {
genInstSetThm(bVarsThm, bVarsTrig, termInst, instSetThm);
}
{
for(std::vector<std::vector<Expr> >::iterator i=instSetThm.begin(), iend=instSetThm.end(); i!=iend; ++i) {
enqueueInst(univ, *i, null_expr);//fix the null_expr here asap
TRACE("quant inst", "insert mult inst", univ.toString(), " | with bind: "+vectorExpr2string(*i));
}
}
}
*/
/*
void TheoryQuant::synPartInst(const Theorem & univ, const CDList<Expr>& allterms, size_t tBegin ){
const Expr& quantExpr = univ.getExpr();
TRACE("quant inst", "try part with ", quantExpr.toString() , " ");
const std::vector<Trigger>& triggers = d_partTrigs[quantExpr];
std::vector<std::vector<Expr> > instSetThm; //set of instantiations for the thm
std::vector<std::vector<Expr> > termInst; //terminst are bindings, in the order of bVarsTrig
std::vector<Expr> bVarsTrig;
std::vector<Expr> instGterms;
for( std::vector<Trigger>::const_iterator i= triggers.begin(), iend=triggers.end();i!=iend;++i) {
Trigger trig = *i;
TRACE("quant inst","handle part trigger", trig.getEx().toString(),"");
termInst.clear();
bVarsTrig.clear();
instSetThm.clear();
// if(hasGoodSynInstNewTrig(trig, bVarsTrig, termInst, instGterms,allterms, tBegin)) {
if(hasGoodSynInstNewTrig(trig, trig.getBVs(), termInst, instGterms,allterms, tBegin)) {
TRACE("quant syninst", "has good ", termInst.size(),"");
TRACE("quant syninst", "after good ",instSetThm.size(), "");
Theorem newUniv = d_rules->adjustVarUniv(univ, trig.getBVs());
TRACE("quant syninst", " new univ:" ,newUniv.toString(),"");
{
for(size_t i = 0; i< termInst.size(); i++){
const std::vector<Expr>& binds = termInst[i];
const Expr& gterm = instGterms[i];
enqueueInst(newUniv, binds, gterm);
TRACE("quant yeting inst", "instantiating =========", "" , "");
TRACE("quant yeting inst", "instantiating", newUniv.getExpr().toString(), " | with bind: "+vectorExpr2string(binds));
TRACE("quant yeting inst", "instantiating org ", univ.getExpr().toString(), " | with gterm "+gterm.toString());
}
}
}
}
}
*/
void TheoryQuant::semInst(const Theorem & univ, size_t tBegin){
}
void TheoryQuant::checkSat(bool fullEffort){
if(*d_translate) return;
if(d_rawUnivs.size() <=0 ) return;
DebugAssert(d_univsQueue.size() == 0, "something left in d_univsQueue");
DebugAssert(d_simplifiedThmQueue.size() == 0, "something left in d_univsQueue");
#ifdef DEBUG
if(fullEffort){
if( CVC3::debugger.trace("quant assertfact") ){
cout<<"===========all cached univs =========="<<endl;
// for (ExprMap<Theorem>::iterator i=d_simpUnivs.begin(), iend=d_simpUnivs.end(); i!=iend; i++){
// cout<<"------------------------------------"<<endl;
// cout<<(i->first).toString()<<endl;
// cout<<"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~"<<endl;
// cout<<(i->second).getExpr().toString()<<endl;
//}
}
if( CVC3::debugger.trace("quant samehead") ){
cout<<"===========all cached =========="<<endl;
for (ExprMap< CDList<Expr>*>::iterator i=d_same_head_expr.begin(), iend=d_same_head_expr.end(); i!=iend; i++){
cout<<"------------------------------------"<<endl;
cout<<(i->first)<<endl;
cout<<"_______________________"<<endl;
CDList<Expr> * terms= i->second;
for(size_t i =0; i<terms->size(); i++){
cout<<(*terms)[i]<<endl;
}
}
}
}
#endif
#ifdef DEBUG
if( CVC3::debugger.trace("quant checksat") ){
const CDList<Expr>& allpreds = theoryCore()->getPredicates();
cout<<"=========== cur pred & terms =========="<<endl;
for (size_t i=d_lastPredsPos; i<allpreds.size(); i++){
cout<<"i="<<allpreds[i].getIndex()<<" :"<<findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;
}
const CDList<Expr>& allterms = theoryCore()->getTerms();
for (size_t i=d_lastTermsPos; i<allterms.size(); i++){
cout<<"i="<<allterms[i].getIndex()<<" :"<<findExpr(allterms[i])<<"|"<<allterms[i]<<endl;
}
cout<<"=========== cur quant =========="<<endl;
for (size_t i=0; i<d_univs.size(); i++){
cout<<"i="<<d_univs[i].getExpr().getIndex()<<" :"<<findExpr(d_univs[i].getExpr())<<"|"<<d_univs[i]<<endl;
}
}
if( CVC3::debugger.trace("quant checksat equ") ){
const CDList<Expr>& allpreds = theoryCore()->getPredicates();
cout<<"=========== cur pred equ =========="<<endl;
for (size_t i=d_lastPredsPos; i<allpreds.size(); i++){
if(allpreds[i].isEq()){
cout<<"i="<<allpreds[i].getIndex()<<" :"<<findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;
}
}
cout<<"=========== cur pred equ end =========="<<endl;
}
#endif
if((*d_useLazyInst && !fullEffort) ) return;
{//for the same head list
const CDList<Expr>& allterms = theoryCore()->getTerms();
for(size_t i=d_lastTermsPos; i<allterms.size(); i++){
Expr t = allterms[i];
if(canGetHead(t)){
if(d_same_head_expr.count(getHead(t)) >0){
d_same_head_expr[getHead(t)]->push_back(t);
}
else{
d_same_head_expr[getHead(t)]=
new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
d_same_head_expr[getHead(t)]->push_back(t);
}
}
}
const CDList<Expr>& allpreds = theoryCore()->getPredicates();
for(size_t i=d_lastPredsPos; i<allpreds.size(); i++){
Expr t = allpreds[i];
if(canGetHead(t)){
if(d_same_head_expr.count(getHead(t)) >0){
d_same_head_expr[getHead(t)]->push_back(t);
}
else{
d_same_head_expr[getHead(t)]=
new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
d_same_head_expr[getHead(t)]->push_back(t);
}
}
}
}
{//for the equalities list
const CDList<Expr>& allpreds = theoryCore()->getPredicates();
for(size_t i=d_lastPredsPos; i<allpreds.size(); i++){
const Expr& t = allpreds[i];
if(t.isEq()){
// cout<<"EQ: "<<t<<endl;
const Expr lterm = t[0];
const Expr rterm = t[1];
d_eqs.push_back(lterm);
d_eqs.push_back(rterm);
/*
ExprMap<CDList<Expr>* >::iterator iter = d_eq_list.find(lterm);
if(d_eq_list.end() == iter){
d_eq_list[lterm] = new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
d_eq_list[lterm]->push_back(rterm);
}
else{
iter->second->push_back(rterm);
}
// cout<<"LTERM: " <<rterm<<endl;
iter = d_eq_list.find(rterm);
if(d_eq_list.end() == iter){
d_eq_list[rterm] = new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
d_eq_list[rterm]->push_back(lterm);
}
else{
iter->second->push_back(lterm);
}
// cout<<"RTERM: " <<lterm<<endl;
*/
}
}
}
{//for rw heuristic
const CDList<Expr>& allterms = theoryCore()->getTerms();
for(size_t i=d_lastTermsPos; i<allterms.size(); i++){
const Expr& cur=allterms[i];
if(READ == cur.getKind() || WRITE == cur.getKind()){
arrayIndexName(cur);
}
}
}
d_instThisRound = 0;
d_useMultTrig=*d_useMult;
d_usePartTrig=*d_usePart;
d_useFullTrig=true;
if(fullEffort) {
d_inEnd=true;
}
else{
d_inEnd=false;
}
ExprMap<ExprMap<vector<dynTrig>* >* > new_trigs;
for(size_t i=d_univs.size(); i<d_rawUnivs.size(); i++){
setupTriggers(new_trigs, d_rawUnivs[i], i);
}
try {
if (!(*d_useNew)){
naiveCheckSat(fullEffort);
}
else if (*d_useSemMatch){
semCheckSat(fullEffort);
}
else {
synCheckSat(new_trigs, fullEffort);
}
}
catch (int x){
while(!d_simplifiedThmQueue.empty()){
d_simplifiedThmQueue.pop();
}
d_tempBinds.clear();
saveContext();
delNewTrigs(new_trigs);
return;
}
sendInstNew();
saveContext();
try{
if((*d_useNew) && (0 == d_instThisRound) && fullEffort && theoryCore()->getTerms().size()< (size_t)(*d_maxNaiveCall) ) {
// cout<<"naive called"<<endl;
if (0== theoryCore()->getTerms().size()){
static int counter =0;
std::set<Expr> types;
for(size_t i = 0; i<d_univs.size(); i++){
const Expr& cur_quant = d_univs[i].getExpr();
const std::vector<Expr> cur_vars = cur_quant.getVars();
for(size_t j =0; j<cur_vars.size(); j++){
types.insert(cur_vars[j].getType().getExpr());
}
}
std::string base("_naiveInst");
for(std::set<Expr>::iterator i=types.begin(), iend = types.end(); i != iend; i++){
counter++;
std::stringstream tempout;
tempout << counter;
std::string out_str = base + tempout.str();
Expr newExpr = theoryCore()->getEM()->newVarExpr(out_str);
newExpr.setType(Type(*i));
Proof pf;
Expr newExpr2 = theoryCore()->getEM()->newVarExpr(out_str+"extra");
newExpr2.setType(Type(*i));
Expr newConstThm;
if(Type(*i) == theoryCore()->getEM()->newRatExpr(0).getType()){
//somehow theory_arith will complain if we use expr2 to form the eq here
newConstThm = newExpr.eqExpr(theoryCore()->getEM()->newRatExpr(0));
}
else{
newConstThm = newExpr.eqExpr(newExpr2);
}
Theorem newThm = d_rules->addNewConst(newConstThm);
enqueueFact(newThm);
d_tempBinds.clear();
return;
}
}
naiveCheckSat(fullEffort);
}
}//end of try
catch (int x){
// d_simplifiedThmQueue.clear();
while(!d_simplifiedThmQueue.empty()){
d_simplifiedThmQueue.pop();
}
d_tempBinds.clear();
saveContext();
delNewTrigs(new_trigs);
return;
}
if(fullEffort) {
sendInstNew();
}
combineOldNewTrigs(new_trigs);
delNewTrigs(new_trigs);
}
void TheoryQuant::saveContext(){
d_lastArrayPos.set(d_arrayTrigs.size());
d_univsSavedPos.set(d_univs.size());
d_rawUnivsSavedPos.set(d_rawUnivs.size());
d_lastTermsPos.set(theoryCore()->getTerms().size());
d_lastPredsPos.set(theoryCore()->getPredicates().size());
d_lastUsefulGtermsPos.set(d_usefulGterms.size());
}
/*void TheoryQuant::synCheckSat(bool fullEffort){
}
*/
void TheoryQuant::synCheckSat(ExprMap<ExprMap<vector<dynTrig>* >* >& new_trigs, bool fullEffort){
d_allout=false;
if(fullEffort) {
setIncomplete("Quantifier instantiation");
}
size_t uSize = d_univs.size() ;
const CDList<Expr>& allterms = theoryCore()->getTerms();
const CDList<Expr>& allpreds = theoryCore()->getPredicates();
size_t tSize = allterms.size();
size_t pSize = allpreds.size();
TRACE("quant",uSize, " uSize and univsSavedPOS ", d_univsSavedPos);
TRACE("quant",tSize, " tSize and termsLastPos ", d_lastTermsPos);
TRACE("quant",pSize, " pSize and predsLastPos ", d_lastPredsPos);
TRACE("quant", fullEffort, " fulleffort:scope ",theoryCore()->getCM()->scopeLevel() );
for(size_t i=d_lastTermsPos; i<tSize; i++){
const Expr& cur(allterms[i]);
if(usefulInMatch(cur)){
if(*d_useExprScore){
int score = getExprScore(cur);
if(score <= d_curMaxExprScore && 0 <= score ){
d_usefulGterms.push_back(cur);
add_parent(cur);
}
}
else{
d_usefulGterms.push_back(cur);
add_parent(cur);
}
}
else{
}
}
for(size_t i=d_lastPredsPos; i<pSize; i++){
const Expr& cur=allpreds[i];
if( usefulInMatch(cur)){
if(*d_useExprScore ){
int score = getExprScore(cur);
if(score <= d_curMaxExprScore && 0 <= score){
d_usefulGterms.push_back(cur);
add_parent(cur);
}
}
else{
d_usefulGterms.push_back(cur);
add_parent(cur);
}
}
else{
}
}
if(d_useFullTrig && d_inEnd && *d_useInstEnd ){
if(*d_useExprScore){
matchListOld(d_usefulGterms, d_lastUsefulGtermsPos, d_usefulGterms.size() ); //new terms to old list
matchListNew(new_trigs, d_usefulGterms, 0, d_usefulGterms.size()); //new and old terms to new list
if(sendInstNew() > 0){
TRACE("inend", "debug 1", "" ,"" );
return;
}
d_allout = true;
{
CDList<Expr>* changed_terms = new (false) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
collectChangedTerms(*changed_terms);
matchListOld(*changed_terms, 0, changed_terms->size());
matchListNew(new_trigs, *changed_terms, 0 , changed_terms->size());
delete changed_terms;
}
int n;
if( ( n = sendInstNew()) > 0){
TRACE("inend", "debug 2", " # ",n );
return;
}
d_allout = false;
int numNewTerm=0;
int oldNum=d_usefulGterms.size();
for(size_t i=0; i<tSize; i++){
const Expr& cur(allterms[i]);
if(!(usefulInMatch(cur))) continue;
int score = getExprScore(cur);
if( score > d_curMaxExprScore){
if((d_curMaxExprScore + 1) == score){
d_usefulGterms.push_back(cur);
add_parent(cur);
numNewTerm++;
}
else{
TRACE("inend", "is this good? ", cur.toString()+" #-# " , score);
d_usefulGterms.push_back(cur);
add_parent(cur);
numNewTerm++;
}
}
}
for(size_t i=0; i<pSize; i++){
const Expr& cur(allpreds[i]);
if(!(usefulInMatch(cur))) continue;
int score = getExprScore(cur);
if( score > d_curMaxExprScore){
if((d_curMaxExprScore + 1) == score){
d_usefulGterms.push_back(cur);
add_parent(cur);
numNewTerm++;
}
else{
TRACE("inend", "is this good? ", cur.toString()+" #-# " , score);
d_usefulGterms.push_back(cur);
add_parent(cur);
numNewTerm++;
}
}
}
if(numNewTerm >0 ){
if(d_curMaxExprScore >=0 ){
d_curMaxExprScore = d_curMaxExprScore+1;;
}
else {
d_curMaxExprScore = d_curMaxExprScore+1;
}
matchListOld(d_usefulGterms, oldNum, d_usefulGterms.size() );
matchListNew(new_trigs, d_usefulGterms, oldNum, d_usefulGterms.size());
if(sendInstNew() > 0){
TRACE("inend", "debug 3", "" , "" );
return;
}
}
for(size_t array_index = 0; array_index < d_arrayTrigs.size(); array_index++){
arrayHeuristic(d_arrayTrigs[array_index].trig, d_arrayTrigs[array_index].univ_id);
}
return ;
}
TRACE("inend", "debug 3 0", "", "");
TRACE("quant","this round; ",d_callThisRound,"");
return;
}
if ((uSize == d_univsSavedPos) &&
(tSize == d_lastTermsPos) &&
(pSize == d_lastPredsPos) ) return;
matchListOld(d_usefulGterms, d_lastUsefulGtermsPos,d_usefulGterms.size() ); //new terms to old list
matchListNew(new_trigs, d_usefulGterms, 0, d_usefulGterms.size() ); //new and old terms to new list
for(size_t array_index = d_lastArrayPos; array_index < d_arrayTrigs.size(); array_index++){
arrayHeuristic(d_arrayTrigs[array_index].trig, d_arrayTrigs[array_index].univ_id);
}
TRACE("quant","this round; ",d_callThisRound,"");
return;
}
void TheoryQuant::semCheckSat(bool fullEffort){
}
//the following is old code and I did not modify much, Yeting
void TheoryQuant::naiveCheckSat(bool fullEffort){
TRACE("quant", "checkSat ", fullEffort, "{");
IF_DEBUG(int instCount = d_instCount);
size_t uSize = d_univs.size(), stSize = d_savedTerms.size();
if(true || (fullEffort && uSize > 0)) {
// First of all, this algorithm is incomplete
setIncomplete("Quantifier instantiation");
if(d_instCount>=*d_maxQuantInst)
return;
//first attempt to instantiate with the saved terms
//only do this if there are new saved terms or new theroems and
// at least some saved terms
bool savedOnly = ((uSize > d_univsSavedPos.get() && stSize > 0) ||
(stSize > d_savedTermsPos.get()));
int origCount = d_instCount;
if(savedOnly)
{
TRACE("quant", "checkSat [saved insts]: univs size = ", uSize , " ");
for(size_t i=0, pos = d_univsSavedPos.get(); i<uSize; i++) {
if(d_instCount>= *d_maxQuantInst)
break;
else
instantiate(d_univs[i], i>=pos, true, d_savedTermsPos.get());
}
d_univsSavedPos.set(d_univs.size());
d_savedTermsPos.set(stSize);
}
if(!savedOnly || d_instCount == origCount)
{ //instantiate with context dependent assertions terms
TRACE("quant", "checkSat [context insts]: univs size = ", uSize , " ");
const CDList<Expr>& assertions = theoryCore()->getTerms();
int origSize = d_contextTerms.size();
// for(size_t i=0; i<uSize; i++)
// assertions.push_back(d_univs[i].getExpr());
//build the map of all terms grouped into vectors by types
TRACE("quant", "checkSat terms size = ", assertions.size() , " ");
mapTermsByType(assertions);
for(size_t i=0, pos = d_univsContextPos.get(); i<uSize; i++) {
if(d_instCount>= *d_maxQuantInst)
break;
else
instantiate(d_univs[i], i>=pos, false, origSize);
}
d_univsContextPos.set(d_univs.size());
}
TRACE("quant terse", "checkSat total insts: ",
d_instCount, ", new "+int2string(d_instCount - instCount));
}
TRACE("quant", "checkSat total insts: ", d_instCount, " ");
TRACE("quant", "checkSat new insts: ", d_instCount - instCount, " ");
TRACE("quant", "checkSat effort:", fullEffort, " }");
}
/*! \brief Queues up all possible instantiations of bound
* variables.
*
* The savedMap boolean indicates whether to use savedMap or
* d_contextMap the all boolean indicates weather to use all
* instantiation or only new ones and newIndex is the index where
* new instantiations begin.
*/
void TheoryQuant::instantiate(Theorem univ, bool all, bool savedMap,
size_t newIndex)
{
if(!all && ((savedMap && newIndex == d_savedTerms.size())
||(!savedMap && newIndex == d_contextTerms.size())))
return;
TRACE("quant", "instanitate", all , "{");
std::vector<Expr> varReplacements;
recInstantiate(univ, all, savedMap, newIndex, varReplacements);
TRACE("quant", "instanitate", "", "}");
}
//! does most of the work of the instantiate function.
void TheoryQuant::recInstantiate(Theorem& univ, bool all, bool savedMap,
size_t newIndex,
std::vector<Expr>& varReplacements)
{
Expr quantExpr = univ.getExpr();
const vector<Expr>& boundVars = quantExpr.getVars();
size_t curPos = varReplacements.size();
TRACE("quant", "recInstantiate: ", boundVars.size() - curPos, "");
//base case: a full vector of instantiations exists
if(curPos == boundVars.size()) {
if(!all)
return;
Theorem t = d_rules->universalInst(univ, varReplacements);
d_insts[t.getExpr()] = varReplacements;
TRACE("quant", "recInstantiate => " , t.toString(), "");
if(d_instCount< *d_maxQuantInst) {
d_instCount=d_instCount+1;
enqueueInst(univ, varReplacements, null_expr);
// enqueueInst(univ, t);
// enqueueFact(t);
}
return;
}
//recursively add all possible instantiations in the next
//available space of the vector
else {
Type t = getBaseType(boundVars[curPos]);
int iendC=0, iendS=0, iend;
std::vector<size_t>* typeVec = NULL; // = d_savedMap[t];
CDList<size_t>* typeList = NULL; // = *d_contextMap[t];
if(d_savedMap.count(t) > 0) {
typeVec = &(d_savedMap[t]);
iendS = typeVec->size();
TRACE("quant", "adding from savedMap: ", iendS, "");
}
if(!savedMap) {
if(d_contextMap.count(t) > 0) {
typeList = d_contextMap[t];
iendC = typeList->size();
TRACE("quant", "adding from contextMap:", iendC , "");
}
}
iend = iendC + iendS;
for(int i =0; i<iend; i++) {
TRACE("quant", "I must have gotten here!", "", "");
size_t index;
if(i<iendS){
index = (*typeVec)[i];
varReplacements.push_back(d_savedTerms[index]);
}
else {
index = (*typeList)[i-iendS];
varReplacements.push_back(d_contextTerms[index]);
}
if((index < newIndex) || (!savedMap && i<iendS))
recInstantiate(univ, all, savedMap, newIndex, varReplacements);
else
recInstantiate(univ, true, savedMap, newIndex, varReplacements);
varReplacements.pop_back();
}
}
}
/*! \brief categorizes all the terms contained in a vector of expressions by
* type.
*
* Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
*/
void TheoryQuant::mapTermsByType(const CDList<Expr>& terms)
{
Expr trExpr=trueExpr(), flsExpr = falseExpr();
Type boolT = boolType();
if(d_contextMap.count(boolT) == 0)
{
d_contextMap[boolT] =
new(true) CDList<size_t>(theoryCore()->getCM()->getCurrentContext());
size_t pos = d_contextTerms.size();
d_contextTerms.push_back(trExpr);
d_contextTerms.push_back(flsExpr);
(*d_contextMap[boolT]).push_back(pos);
(*d_contextMap[boolT]).push_back(pos+1);
}
for(size_t i=0; i<terms.size(); i++)
recursiveMap(terms[i]);
// Add all our saved universals to the pool
for(size_t i=0; i<d_univs.size(); i++)
recursiveMap(d_univs[i].getExpr());
}
/*! \brief categorizes all the terms contained in an expressions by
* type.
*
* Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
* returns true if the expression does not contain bound variables, false
* otherwise.
*/
bool TheoryQuant::recursiveMap(const Expr& e)
{
if(d_contextCache.count(e)>0) {
return(d_contextCache[e]);
}
if(e.arity()>0) {
for(Expr::iterator it = e.begin(), iend = e.end(); it!=iend; ++it)
//maps the children and returns a bool
if(recursiveMap(*it) == false) {
d_contextCache[e] = false;
}
}
else if(e.getKind() == EXISTS || e.getKind() == FORALL){
//maps the body
if(recursiveMap(e.getBody())==false) {
d_contextCache[e]=false;
}
}
//found a bound variable in the children
if(d_contextCache.count(e)>0) {
return false;
}
if(d_savedCache.count(e) > 0) {
return true;
}
Type type = getBaseType(e);
if(!type.isBool() && !(e.getKind()==BOUND_VAR)){
TRACE("quant", "recursiveMap: found ",
e.toString() + " of type " + type.toString(), "");
int pos = d_contextTerms.size();
d_contextTerms.push_back(e);
if(d_contextMap.count(type)==0)
d_contextMap[type] =
new(true) CDList<size_t>(theoryCore()->getCM()->getCurrentContext());
(*d_contextMap[type]).push_back(pos);
}
if(e.getKind() == BOUND_VAR) {
d_contextCache[e] = false;
return false;
}
else {
d_contextCache[e] = true;
return true;
}
//need to implement:
//insert all instantiations if type is finite and reasonable
//also need to implement instantiations of subtypes
}
/*!\brief Used to notify the quantifier algorithm of possible
* instantiations that were used in proving a context inconsistent.
*/
void TheoryQuant::notifyInconsistent(const Theorem& thm){
#ifdef DEBUG
if( CVC3::debugger.trace("quant inscon") ){
cout<<"the one caused incsonsistency"<<endl;
cout<<thm.getAssumptionsRef().toString()<<endl;
std::vector<Expr> assump;
thm.getLeafAssumptions(assump);
cout<<"===========leaf assumptions; =========="<<endl;
for(std::vector<Expr>::iterator i=assump.begin(), iend=assump.end(); i!=iend; i++){
cout<<">>"<<i->toString()<<endl;
}
}
#endif
if(d_univs.size() == 0)
return;
DebugAssert(thm.getExpr().isFalse(), "notifyInconsistent called with"
" theorem: " + thm.toString() + " which is not a derivation of false");
TRACE("quant", "notifyInconsistent: { " , thm.toString(), "}");
// thm.clearAllFlags();
// findInstAssumptions(thm);
TRACE("quant terse", "notifyInconsistent: savedTerms size = ",
d_savedTerms.size(), "");
TRACE("quant terse", "last term: ",
d_savedTerms.size()? d_savedTerms.back() : Expr(), "");
}
/*! \brief A recursive function used to find instantiated universals
* in the hierarchy of assumptions.
*/
void TheoryQuant::findInstAssumptions(const Theorem& thm)
{
if(thm.isNull() || thm.isRefl() || thm.isFlagged())
return;
thm.setFlag();
const Expr& e = thm.getExpr();
if(d_insts.count(e) > 0) {
vector<Expr>& insts = d_insts[e];
int pos;
for(vector<Expr>::iterator it = insts.begin(), iend = insts.end(); it!=iend
; ++it)
{
if(d_savedCache.count(*it) == 0) {
TRACE("quant", "notifyInconsistent: found:", (*it).toString(), "");
d_savedCache[*it] = true;
pos = d_savedTerms.size();
d_savedTerms.push_back(*it);
d_savedMap[getBaseType(*it)].push_back(pos);
}
}
}
if(thm.isAssump())
return;
const Assumptions& a = thm.getAssumptionsRef();
for(Assumptions::iterator it =a.begin(), iend = a.end(); it!=iend; ++it){
findInstAssumptions(*it);
}
}
//! computes the type of a quantified term. Always a boolean.
void TheoryQuant::computeType(const Expr& e)
{
switch (e.getKind()) {
case FORALL:
case EXISTS: {
if(!e.getBody().getType().isBool())
throw TypecheckException("Type mismatch for expression:\n\n "
+ e.getBody().toString()
+ "\n\nhas the following type:\n\n "
+ e.getBody().getType().toString()
+ "\n\nbut the expected type is Boolean:\n\n ");
else
e.setType(e.getBody().getType());
break;
}
default:
DebugAssert(false,"Unexpected kind in Quantifier Theory: "
+ e.toString());
break;
}
}
/*!
* TCC(forall x.phi(x)) = (forall x. TCC(phi(x)))
* OR (exists x. TCC(phi(x)) & !phi(x))
* TCC(exists x.phi(x)) = (forall x. TCC(phi(x)))
* OR (exists x. TCC(phi(x)) & phi(x))
*/
Expr TheoryQuant::computeTCC(const Expr& e) {
DebugAssert(e.isQuantifier(), "Unexpected expression in Quantifier Theory: "
+ e.toString());
bool forall(e.getKind() == FORALL);
const Expr& phi = e.getBody();
Expr tcc_phi = getTCC(phi);
Expr forall_tcc = getEM()->newClosureExpr(FORALL, e.getVars(), tcc_phi);
Expr exists_tcc = getEM()->newClosureExpr(EXISTS, e.getVars(),
tcc_phi && (forall? !phi : phi));
return (forall_tcc || exists_tcc);
}
ExprStream&
TheoryQuant::print(ExprStream& os, const Expr& e) {
switch(os.lang()) {
case SIMPLIFY_LANG:
{
switch(e.getKind()){
case FORALL:
case EXISTS: {
if(!e.isQuantifier()) {
e.print(os);
break;
}
os << "(" << ((e.getKind() == FORALL)? "FORALL" : "EXISTS");
const vector<Expr>& vars = e.getVars();
bool first(true);
os << "(" ;
for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
i!=iend; ++i) {
if(first) first = false;
else os << " " ;
os << *i;
// The quantifier may be in a raw parsed form, in which case
// the type is not assigned yet
//if(i->isVar()) // simplify do not need type
// os << ":" << space << pushdag << (*i).getType() << popdag;
}
os << ") " << e.getBody() << ")";
}
break;
default:
e.print(os);
break;
}
break;
}
case PRESENTATION_LANG: {
switch(e.getKind()){
case FORALL:
case EXISTS: {
if(!e.isQuantifier()) {
e.print(os);
break;
}
os << "(" << push << ((e.getKind() == FORALL)? "FORALL" : "EXISTS")
<< space << push;
const vector<Expr>& vars = e.getVars();
bool first(true);
os << "(" << push;
for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
i!=iend; ++i) {
if(first) first = false;
else os << push << "," << pop << space;
os << *i;
// The quantifier may be in a raw parsed form, in which case
// the type is not assigned yet
// the following lines are changed for a neat output / by yeting
if(*d_translate || true){
if(i->isVar())
os << ":" << space << pushdag << (*i).getType() << popdag;
}
}
os << push << "): " << pushdag << push
<< e.getBody() << push << ")";
}
break;
default:
e.print(os);
break;
}
break;
}
case SMTLIB_LANG: {
d_theoryUsed = true;
switch(e.getKind()){
case FORALL:
case EXISTS: {
if(!e.isQuantifier()) {
e.print(os);
break;
}
os << "(" << push << ((e.getKind() == FORALL)? "forall" : "exists")
<< space;
const vector<Expr>& vars = e.getVars();
bool first(true);
// os << "(" << push;
for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
i!=iend; ++i) {
if(first) first = false;
else os << space;
os << "(" << push << *i;
// The quantifier may be in a raw parsed form, in which case
// the type is not assigned yet
if(i->isVar())
os << space << pushdag << (*i).getType() << popdag;
os << push << ")" << pop << pop;
}
os << space << pushdag
<< e.getBody() << push << ")";
break;
}
default:
throw SmtlibException("TheoryQuant::print: SMTLIB_LANG: Unexpected expression: "
+getEM()->getKindName(e.getKind()));
break;
}
break;
} // End of SMTLIB_LANG
case LISP_LANG: {
switch(e.getKind()){
case FORALL:
case EXISTS: {
if(!e.isQuantifier()) {
e.print(os);
break;
}
os << "(" << push << ((e.getKind() == FORALL)? "FORALL" : "EXISTS")
<< space;
const vector<Expr>& vars = e.getVars();
bool first(true);
os << "(" << push;
for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
i!=iend; ++i) {
if(first) first = false;
else os << space;
os << "(" << push << *i;
// The quantifier may be in a raw parsed form, in which case
// the type is not assigned yet
if(i->isVar())
os << space << pushdag << (*i).getType() << popdag;
os << push << ")" << pop << pop;
}
os << push << ")" << pop << pop << pushdag
<< e.getBody() << push << ")";
}
break;
default:
e.print(os);
break;
}
break;
}
default:
e.print(os);
break;
}
return os;
}
///////////////////////////////////////////////////////////////////////////////
//parseExprOp:
//translating special Exprs to regular EXPR??
///////////////////////////////////////////////////////////////////////////////
Expr
TheoryQuant::parseExprOp(const Expr& e) {
TRACE("parser", "TheoryQuant::parseExprOp(", e, ")");
// If the expression is not a list, it must have been already
// parsed, so just return it as is.
if(RAW_LIST != e.getKind()) return e;
DebugAssert(e.arity() > 0,
"TheoryQuant::parseExprOp:\n e = "+e.toString());
const Expr& c1 = e[0][0];
const string& opName(c1.getString());
int kind = getEM()->getKind(opName);
switch(kind) {
case FORALL:
case EXISTS: { // (OP ((v1 ... vn tp1) ...) body)
if(!(e.arity() == 3 && e[1].getKind() == RAW_LIST && e[1].arity() > 0))
throw ParserException("Bad "+opName+" expression: "+e.toString());
// Iterate through the groups of bound variables
vector<pair<string,Type> > vars; // temporary stack of bound variables
for(Expr::iterator i=e[1].begin(), iend=e[1].end(); i!=iend; ++i) {
if(i->getKind() != RAW_LIST || i->arity() < 2)
throw ParserException("Bad variable declaration block in "+opName
+" expression: "+i->toString()
+"\n e = "+e.toString());
// Iterate through individual bound vars in the group. The
// last element is the type, which we have to rebuild and
// parse, since it is used in the creation of bound variables.
Type tp(parseExpr((*i)[i->arity()-1]));
if (tp == boolType()) {
throw ParserException("A quantified variable may not be of type BOOLEAN");
}
for(int j=0, jend=i->arity()-1; j<jend; ++j) {
if((*i)[j].getKind() != ID)
throw ParserException("Bad variable declaration in "+opName+""
" expression: "+(*i)[j].toString()+
"\n e = "+e.toString());
vars.push_back(pair<string,Type>((*i)[j][0].getString(), tp));
}
}
// Create all the bound vars and save them in a vector
vector<Expr> boundVars;
for(vector<pair<string,Type> >::iterator i=vars.begin(), iend=vars.end();
i!=iend; ++i)
boundVars.push_back(addBoundVar(i->first, i->second));
// Rebuild the body
Expr body(parseExpr(e[2]));
// Build the resulting Expr as (OP (vars) body)
Expr res = getEM()->newClosureExpr((kind == FORALL) ? FORALL : EXISTS,
boundVars, body);
return res;
break;
}
default:
DebugAssert(false,
"TheoryQuant::parseExprOp: invalid command or expression: " + e.toString());
break;
}
return e;
}
syntax highlighted by Code2HTML, v. 0.9.1