Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix bug in which equality constraints implied by unification during a… #56

Merged
merged 1 commit into from
Apr 17, 2024
Merged

Fix bug in which equality constraints implied by unification during a… #56

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 50 additions & 1 deletion Src/Core/Common/Rules/CoreRule.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@
using Compiler;
using Extras;
using Terms;
using Z3BoolExpr = Z3.BoolExpr;

internal class CoreRule
{
Expand Down Expand Up @@ -777,6 +778,8 @@ public virtual void Execute(
return;
}

index.BeginJoinMatch();

Term pattern;
FindData otherFind;
Matcher otherMatcher;
Expand Down Expand Up @@ -823,7 +826,7 @@ public virtual void Execute(
ApplyMatch(index, otherMatcher, tp, ConstraintNode.BLSecond))
{
Contract.Assert(headNode.Binding != null);
Pend(
PendJoinMatch(
keepDerivations,
index,
pending,
Expand All @@ -833,9 +836,13 @@ public virtual void Execute(

UndoPropagation(ConstraintNode.BLSecond);
}

index.ResetJoinConstraints();
}

UndoPropagation(ConstraintNode.BLFirst);

index.EndJoinMatch();
}

public virtual void Execute(
Expand Down Expand Up @@ -1175,6 +1182,42 @@ protected void Pend(
dervs.Add(d);
}

protected void PendJoinMatch(
bool keepDerivations,
SymExecuter index,
Map<Term, Set<Derivation>> pending,
Term t,
Term bind1,
Term bind2)
{
// TODO: handle this case
if (!keepDerivations)
{
if (!index.Exists(t) && !pending.ContainsKey(t))
{
pending.Add(t, null);
}

return;
}

var d = new Derivation(this, bind1, bind2, new List<Z3BoolExpr>(index.GetPendingJoinConstraints()));
if (index.IfExistsThenDerive(t, d))
{
index.AddJoinDerivation(t, bind1, bind2);
return;
}

Set<Derivation> dervs;
if (!pending.TryFindValue(t, out dervs))
{
dervs = new Set<Derivation>(Derivation.Compare);
pending.Add(t, dervs);
}

dervs.Add(d);
}

protected void Pend(
bool keepDerivations,
Executer index,
Expand Down Expand Up @@ -2386,6 +2429,12 @@ public override bool TryEval(SymExecuter facts, int bindingLevel)
BindingLevel = bindingLevel;
return true;
}
else if (bindSymb.IsVariable)
{
Binding = facts.Index.TrueValue;
BindingLevel = bindingLevel;
return true;
}
else if (!typeBins.TryFindValue(bindSymb, out typeTerm))
{
return false;
Expand Down
20 changes: 20 additions & 0 deletions Src/Core/Common/Rules/Derivation.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@
using Compiler;
using Extras;
using Terms;
using Z3BoolExpr = Z3.BoolExpr;

internal class Derivation
{
Expand All @@ -37,6 +38,12 @@ public Term Binding2
private set;
}

public List<Z3BoolExpr> PendingJoinConstraints
{
get;
private set;
}

/// <summary>
/// Create a derivation for facts
/// </summary>
Expand All @@ -55,6 +62,19 @@ public Derivation(CoreRule rule, Term binding1, Term binding2)
Rule = rule;
Binding1 = binding1;
Binding2 = binding2;
PendingJoinConstraints = new List<Z3BoolExpr>();
}

/// <summary>
/// Absent bindings should be given the value FALSE
/// </summary>
public Derivation(CoreRule rule, Term binding1, Term binding2, List<Z3BoolExpr> pendingConstraints)
{
Contract.Requires(rule != null && binding1 != null && binding2 != null);
Rule = rule;
Binding1 = binding1;
Binding2 = binding2;
PendingJoinConstraints = new List<Z3BoolExpr>(pendingConstraints);
}

public static int Compare(Derivation d1, Derivation d2)
Expand Down
2 changes: 1 addition & 1 deletion Src/Core/Common/Symbols/OpLibrary.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2115,7 +2115,7 @@ internal static Term SymEvaluator_No(SymExecuter facts, Bindable[] values)
{
Contract.Requires(values.Length == 1);
int nResults;
var res = facts.Query(values[0].Binding, out nResults);
var res = facts.QueryNo(values[0].Binding, out nResults);
if (nResults == 0)
{
return facts.Index.TrueValue;
Expand Down
35 changes: 28 additions & 7 deletions Src/Core/Solver/Execution/SymElement.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ public List<ConstraintData> GetConstraintData()

private HashSet<Z3BoolExpr> cachedConstraints = new HashSet<Z3BoolExpr>();

public void AddConstraintData(HashSet<Z3BoolExpr> exprs, Set<Term> posTerms, Set<Term> negTerms)
public void AddConstraintData(HashSet<Z3BoolExpr> exprs, Set<Term> posTerms, Set<Tuple<Term, Set<Tuple<Term, Term>>>> negTerms)
{
bool needToAdd = true;

Expand Down Expand Up @@ -144,10 +144,21 @@ private Z3BoolExpr GetSideConstraints(SymExecuter executer, Set<Term> processed)
localProcessed = new Set<Term>(Term.Compare, processed);
foreach (var negTerm in constraint.NegConstraints)
{
if (!processed.Contains(negTerm) &&
executer.GetSymbolicTerm(negTerm, out next))
if (!processed.Contains(negTerm.Item1) &&
executer.GetSymbolicTerm(negTerm.Item1, out next))
{
var nextConstraint = next.GetSideConstraints(executer, localProcessed);

Z3BoolExpr expr;
foreach (var item in negTerm.Item2)
{
Term normalized;
var expr1 = executer.Encoder.GetTerm(item.Item1, out normalized);
var expr2 = executer.Encoder.GetTerm(item.Item2, out normalized);
expr = executer.Solver.Context.MkEq(expr1, expr2);
nextConstraint = executer.Solver.Context.MkAnd(nextConstraint, expr);
}

nextConstraint = executer.Solver.Context.MkNot(nextConstraint);
currConstraint = CreateAndCacheConstraint(executer, currConstraint, nextConstraint);
}
Expand Down Expand Up @@ -204,9 +215,19 @@ public Z3BoolExpr GetSideConstraints(SymExecuter executer)
{
processed.Clear();
processed.Add(t);
if (executer.GetSymbolicTerm(negTerm, out next))
if (executer.GetSymbolicTerm(negTerm.Item1, out next))
{
var nextConstraint = next.GetSideConstraints(executer, processed);
Z3BoolExpr expr;
foreach (var item in negTerm.Item2)
{
Term normalized;
var expr1 = executer.Encoder.GetTerm(item.Item1, out normalized);
var expr2 = executer.Encoder.GetTerm(item.Item2, out normalized);
expr = executer.Solver.Context.MkEq(expr1, expr2);
nextConstraint = executer.Solver.Context.MkAnd(nextConstraint, expr);
}

nextConstraint = context.MkNot(nextConstraint);
currConstraint = CreateAndCacheConstraint(executer, currConstraint, nextConstraint);
}
Expand Down Expand Up @@ -325,20 +346,20 @@ public Set<Term> PosConstraints
private set;
}

public Set<Term> NegConstraints
public Set<Tuple<Term, Set<Tuple<Term, Term>>>> NegConstraints
{
get;
private set;
}

public ConstraintData(HashSet<Z3BoolExpr> exprs, Set<Term> posTerms, Set<Term> negTerms)
public ConstraintData(HashSet<Z3BoolExpr> exprs, Set<Term> posTerms, Set<Tuple<Term, Set<Tuple<Term, Term>>>> negTerms)
{
DirConstraints = exprs;
PosConstraints = posTerms;
NegConstraints = negTerms;
}

public bool IsSameConstraintData(HashSet<Z3BoolExpr> exprs, Set<Term> posTerms, Set<Term> negTerms)
public bool IsSameConstraintData(HashSet<Z3BoolExpr> exprs, Set<Term> posTerms, Set<Tuple<Term, Set<Tuple<Term, Term>>>> negTerms)
{
if (DirConstraints.SetEquals(exprs) &&
PosConstraints.IsSameSet(posTerms) &&
Expand Down
Loading
Loading