nunoplopes

import math
import operator
from torch._inductor.optimize_indexing import ValueRanges, ValueRangeAnalysis

def neg(x):
    return -x

def reciprocal(x):
    return 1 / x

nunoplopes

def mk_eq(lhs, rhs):
if (
    isinstance(lhs, sympy.Add) and
    isinstance(lhs.args[0], sympy.Integer) and
    isinstance(rhs, sympy.Integer)
):
    return mk_eq(lhs - lhs.args[0], rhs - lhs.args[0])
return sympy.Eq(lhs, rhs)

def simplify_eq(eq):

nunoplopes

diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index b5ed1a070..952f61e29 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -47,18 +47,18 @@ def init_project_def():
     add_lib('ackermannization', ['model', 'rewriter', 'ast', 'solver', 'tactic'], 'ackermannization')
     add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa')
     add_lib('bit_blaster', ['rewriter', 'params'], 'ast/rewriter/bit_blaster')
-    add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core')
-    add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')

nunoplopes

import tensorflow as tf
from tensorflow.contrib.compiler import xla
import numpy as np


a = tf.Variable(1.0, use_resource=True)

def repeat(count, body, vars):
  return tf.while_loop(lambda *args : True, body, vars, maximum_iterations=count)

nunoplopes

diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index 6775409..634d2dc 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -65,6 +65,9 @@ class sat_tactic : public tactic {

             CASSERT("sat_solver", m_solver.check_invariant());
             IF_VERBOSE(TACTIC_VERBOSITY_LVL, m_solver.display_status(verbose_stream()););
+            m_solver.display_dimacs(std::cout);
+            std::flush(std::cout);